A Typed Semantics of Higher-Order Store and Subtyping

Abstract. 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 [14], and relate it to an untyped model by a logical relation. Following the methodology of Reynolds [22], 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.

• Type: Conference
• Year: 2005
• Where: ICTCS
• Authors: Jan Schwinghammer
• Keywords: Call-by-value Language, ICTCS 2005, Intrinsic Denotational Model, Typed Denotational Semantics