Carnegie Mellon University
file.pdf (235.5 kB)
Download file

The Meaning of Types From Intrinsic to Extrinsic Semantics

Download (235.5 kB)
journal contribution
posted on 2005-09-01, 00:00 authored by John C Reynolds
A definition of a typed language is said to be "intrinsic" if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be "extrinsic" if all phrases have meanings that are independent of their typings, while typings represent properties of these meanings. For a simply typed lambda calculus, extended with recursion, subtypes, and named products, we give an intrinsic denotational semantics and a denotational semantics of the underlying untyped language. We then establish a logical relations theorem between these two semantics, and show that the logical relations can be"bracketed" by retractions between the domains of the two semantics. From these results, we derive an extrinsic semantics that uses partial equivalence relations.




Usage metrics