[Prev][Next][Index][Thread]
Type soundness for denotational semantics of state
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
-----------------------------------------------------------------------