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@...
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
-----------------------------------------------------------------------