A Typed Semantics of Higher-Order Store and Subtyping

Jan Schwinghammer

Publication details

Programming Systems

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

@INPROCEEDINGS{schwinghammer:05,
  title = {A Typed Semantics of Higher-Order Store and Subtyping},
  author = {Jan Schwinghammer},
  year = {2005},
  publisher = {{Springer}},
  booktitle = {Italian Conference on Theoretical Computer Science (ICTCS'05)},
  series = {{LNCS}},
  volume = {3701},
  pages = {{390--405}},
}

Legal notice, Privacy policy