[Prev][Next][Index][Thread]
RE: Type soundness for denotational semantics of state
I don't know of a proof based on denotational semantics; why would one
bother?
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.
Bob
@Article{harper:refs-ipl,
author = "Robert Harper",
title = "A Simplified Account of Polymorphic References",
journal = "Information Processing Letters",
year = 1994,
volume = "51",
pages = "201--206"
}
@Article{wright+:type-soundness-ic,
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
-----------------------------------------------------------------------