RE: Type soundness for denotational semantics of state

I don't know of a proof based on denotational semantics; why would one 

Let me mention that Wright and Felleisen and (separately) I gave much 
simpler proofs of soundness for languages with references (among other 
extensions to core ML) based on operational semantics.  Abadi and Cardelli 
have adapted these methods to an object-based language.  No maximal fixed 
points or any similar constructions are required for these proofs.


  author = 	 "Robert Harper",
  title = 	 "A Simplified Account of Polymorphic References",
  journal =	 "Information Processing Letters",
  year =	 1994,
  volume =	 "51",
  pages =	 "201--206"

  author = 	 "Andrew K. Wright and Matthias Felleisen",
  title = 	 "A Syntactic Approach to Type Soundness",
  journal =	 ic,
  year =	 1994,
  volume =	 115,
  number =	 1,
  pages =	 "38--94",
  month =	 "November"

-----Original Message-----
From:	Philip Wadler [SMTP:wadler@research.bell-labs.com]
Sent:	Wednesday, July 16, 1997 2:40 PM
To:	tofte@diku.dk; robin.milner@cl.cam.ac.uk; types@cs.indiana.edu
Subject:	Type soundness for denotational semantics of state

[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

Mads Tofte's thesis contains a (now classic) proof of type
soundness for a language with state, based upon an operational
semantics.  Where would I go to find the same proof for a
denotational semantics, analogous to Milner's original proof
that well-typed programs cannot go wrong?  Thanks, -- P

Philip Wadler                             wadler@research.bell-labs.com
Bell Laboratories             http://cm.bell-labs.com/cm/cs/who/wadler/
Lucent Technologies                             office: +1 908 582 4004
700 Mountain Ave, Room 2T-304                      fax: +1 908 582 5857
Murray Hill, NJ 07974-0636  USA                   home: +1 908 626 9252