Publication details

Saarland University Computer Science

A Typed Semantics of Higher-Order Store and Subtyping

Jan Schwinghammer

Italian Conference on Theoretical Computer Science (ICTCS'05), Vol. 3701 of LNCS, pp. 390--405, Springer, 2005

We consider a call-by-value language, with higher-order functions, records, references to values of arbitrary type, and subtyping. We adapt an intrinsic denotational model for a similar language based on a possible-world semantics, recently given by Levy (2002), and relate it to an untyped model by a logical relation. Following the methodology of Reynolds (2002), this relation is used to establish coherence of the typed semantics, with a coercion interpretation of subtyping. We obtain a typed denotational semantics of (imperative) object-based languages.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009