While many theorems about type systems are provable by straightforward induction, some properties are much trickier to prove and require a clever insight into how to “strengthen the induction hypothesis”. The method of logical relations provides such an insight, and it has been applied, generalized, and extended to prove a variety of interesting properties about typed programs. These include termination, strong normalization, decidability of type checking, consistency of type equivalence, contextual equivalence of programs, effectiveness of data abstraction mechanisms, and validity of program transformations. We will introduce the idea as it originated–Tait’s method for proving termination/strong normalization for the simply-typed lambda calculus–and eventually work our way up to equational reasoning about programs in a language supporting polymorphism, existential types, recursive functions, recursive types, and mutable references. Although the logical relations method is often used in the setting of denotational semantics, we will focus on how to use it to do operational reasoning about typed programs.
A secondary goal of the course is to convey a sense of how one actually does research and makes progress in programming language theory, or at least how I do it. Although classic results are often presented in the literature without any hint of their origins, in reality there is a continual, subtle interplay between the act of proving theorems and the act of discovering what theorems one wants to prove. (This is closely related to what Lakatos calls “the method of proofs and refutations”.) I will try to convey this interplay in the presentation of a number of topics in the course.
Typed Operational Reasoning