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