Lecture type: | Advanced course, 6 CPs |
Time: | Tue & Thu, 10-12 |
Room: | HS001 in E1.3 |
Instructor: | Derek Dreyer |
Teaching assistant: | Georg Neis |
Office Hours: | By appointment |
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.
I taught an earlier version of this course at the University of Chicago in Winter 2006.
Grading: Regular homework assignments (50%), Final exam (25%), Class participation (25%)
Date | Topic | Reading | Homework | |
---|---|---|---|---|
Oct | 21 |
Introduction; Reinventing the basic logical relations method
from first principles; Termination for call-by-value simply-typed lambda-calculus (CBVSTLC) |
TAPL [1]: Chapter 12 (Pierce) | |
23 |
Termination for CBVSTLC, continued; Strong normalization for STLC with full beta-reduction (Tait's method) |
Barendregt [2]: Pages 62-64; Girard [3]: Chapter 6 |
HW #1 out | |
28 | Strong normalization for STLC with full beta-reduction (Tait's method), continued | |||
30 |
Definitional equivalence; Extensional equivalence in the
presence of unit type; How to develop an algorithm for deciding equivalence simultaneously with its proof of correctness |
ATTAPL [4]: Chapter 6 (Crary) | HW #1 due | |
Nov | 4 | Deciding extensional equivalence in the presence of unit, continued | ATTAPL [4]: Chapter 6 (Crary) | HW #2 out |
6 | Deciding extensional equivalence in the presence of unit, continued | ATTAPL [4]: Chapter 6 (Crary) | ||
11 |
Deciding equivalence in the presence of type definitions; Proving consistency in the presence of circular type definitions |
ATTAPL [4]: Chapter 9 (Stone) | HW #2 due | |
13 | Deciding equivalence in the presence of singleton kinds | Stone-Harper [5,6] | HW #3 out | |
18 |
Termination for CBV System F (Girard's method, basic version); Simple, set-based parametricity results |
Girard [3]: Chapters 11, 14; Barendregt [2]: Pages 65-66 |
||
20 |
Strong normalization for System F (Girard's method of candidate sets); Failure of normalization in the presence of type analysis (Girard's J operator); Motivation for relational parametricity |
Gallier [7], Harper-Mitchell [8] | HW #3 due | |
25,27 | Thanksgiving week (no class); Fun reading: Lakatos' Proofs and Refutations | Lakatos [9] | ||
Dec | 2 | Reynolds' relational parametricity; Wadler's "free" theorems (Andreas Rossberg lecturing) | Reynolds [10], Wadler [11] | HW #4 out |
4 | Kennedy's units of measure (a cool application of relational parametricity) | Kennedy [12] |