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.