The method of logical relations is a fundamental tool in type theory that is used to prove termination and normalization and to analyze equations between terms, including parametricity properties for polymorphism. The main idea is to interpret types as relations (of a suitable class) on terms by associating to each type constructor a relational action that determines the relation associated to a compound type as a function of its constituent types. The interpretation is chosen so that well-typed terms stand in the relation associated to their type, and so that related terms satisfy a property of interest, from which it follows that well-typed terms have that property. Logical relations have many applications, but all share the characteristic that a global property of terms is reduced to local properties of types. I will develop the theory of logical relations from first principles, concentrating on two important cases, Goedel's System T and Girard's System F. |