Sciweavers

ENTCS
2007

Syntactic Logical Relations for Polymorphic and Recursive Types

13 years 10 months ago
Syntactic Logical Relations for Polymorphic and Recursive Types
The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed languages, for example to establish contextual equivalences of terms. The chief difficulty in using logical relations is to establish the existence of a suitable relational interpretation. We extend work of Pitts and Birkedal and Harper on constructing relational interpretations of types to polymorphism and recursive types, and apply it to establish parametricity and representation independence properties in a purely operational setting. We argue that, once the existence of a relational interpretation has been established, it is straightforward to use it to establish properties of interest.
Karl Crary, Robert Harper
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Karl Crary, Robert Harper
Comments (0)