Re: Type soundness for denotational semantics of state

To: wadler@research.bell-labs.com (Philip Wadler)
Subject: Re: Type soundness for denotational semantics of state
From: Flemming Nielson <fn@daimi.aau.dk>
Date: Mon, 28 Jul 1997 11:26:15 +0200 (MET DST)
Cc: tofte@diku.dk, robin.milner@cl.cam.ac.uk, types@cs.indiana.edu
Delivery-Date: Mon, 28 Jul 1997 04:49:50 -0500
In-Reply-To: <199707161913.OAA01898@shovelnose.cs.indiana.edu> from Philip Wadler at "Jul 16, 97 02:39:33 pm"

> 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

You will find similar proofs in the second reference below (using
results from the former) in the case of operational semantics and
a functional language with communication (which works much like
references).

Regards, Flemming Nielson
 
@InCollection{PoSuEfint,
  author =       "H. R. Nielson and F. Nielson and T. Amtoft",
  title =        "Polymorphic Subtyping for Effect Analysis: 
                  The Static Semantics",
  booktitle =    "Proceedings of the Fifth {LOMAPS} Workshop",
  publisher =    "Springer-Verlag",
  year =         "1997",
  editor =       "M. Dam",
  number =       "1192",
  series =       "Lecture Notes in Computer Science",
}

@InCollection{PoSuEfsem,
  author =       "T. Amtoft and F. Nielson and H. R. Nielson and J. Ammann",
  title =        "Polymorphic Subtyping for Effect Analysis: 
                  The Dynamic Semantics",
  booktitle =    "Proceedings of the Fifth {LOMAPS} Workshop",
  publisher =    "Springer-Verlag",
  year =         "1997",
  editor =       "M. Dam",
  number =       "1192",
  series =       "Lecture Notes in Computer Science",
}

Prev: Theory of Types and Proofs (TTP) --- Kyoto Meeting, sept. 19-20
Next: Workshop on Theories of Types and Proofs
Index(es):
- Main
- Thread