CMSC 32001-1: Advanced Type Systems

Instructor: Derek Dreyer
Quarter: Winter 2006
Meeting Place: Ryerson 276
Meeting Time: MW 4:00-5:20
Office Hours: By appointment, TTI-C 252
Mailing List:

Course Description: The prerequisite intro course on programming languages (CMSC 32100) has given you some basic vocabulary in the language of type systems. You learned about recursion, polymorphism, static and dynamic semantics, big-step and small-step semantics. You also learned about one of the most basic and ubiquitous tools in modern research on type systems, namely the method of proving type soundness (i.e. type safety) syntactically by progress and preservation. The goal of this advanced course is to further enrich your vocabulary and to expand your arsenal with a new and powerful tool for reasoning about typed programs, namely the method of logical relations.
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, contextual equivalence of programs, and validity of simple 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, data abstraction, recursive functions, and recursive types. 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.
When I say "we" will study and "we" will learn about these various topics, I really mean "we": in some cases I will be learning the material along with you! The topics I have chosen for this course are topics that I am knowledgeable about (to varying degrees) but would really like to understand more deeply, and teaching this course seems like a fun and interactive way to do that.

Grading: The grade is based primarily on homework and class participation. Attendance is mandatory, as some of the material we will be discussing is not adequately covered in the accompanying readings. Please let me know if you cannot attend class. The homeworks will be essentially theoretical in nature (e.g. proving theorems). If you have trouble with them, come talk to me. I am open to meeting with students at any time, but you must schedule an appointment. There will be no final exam. In any case, the workload is not intended to be terribly heavy. Since we are covering so much ground, however, you are unlikely to gain much from the course if you do not put in serious time outside of class to study and fully digest the material.

Textbook: The required textbook for the course is Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce. This is the sequel to Pierce's Types and Programming Languages textbook, and it consists of ten chapters by different experts on, well, a variety of advanced topics in types and programming languages. We will not follow this book very closely, but for certain topics we will rely on it heavily. Regardless, it is an indispensable resource, and you should own both of the Pierce books if you are an aspiring PL researcher. For other topics, we will read selected research papers and excerpts from longer texts. For these I will provide links to PDF files in the bibliography section at the bottom of this page.

Lecture Notes: Aaron Turon has graciously TeXed up lecture notes for a number of the lectures. They are somewhat lacking in expository text, but are very helpful nonetheless. Thank you, Aaron!

Constantly Changing Syllabus

Date Topic Reading Homework
Jan 4 Introduction; Strengthening the induction hypothesis; Proving termination for the call-by-value simply-typed lambda-calculus using logical relations TAPL: Chapter 12 HW #1 Out
Jan 9 Logical relations proof of termination (continued)
Jan 11 No class (POPL week)
Jan 16 No class (MLK, Jr.'s Birthday)
Jan 18 Strong normalization for full reduction in simply-typed lambda-calculus (Tait's method) Girard: Chapter 6; Barendregt: 62-64 HW #1 Due
Jan 20 Make-up class (10:30 AM at TTI-C): Review of HW #1; Tait's method (continued)
Jan 23 Definitional equivalence; Extensional equivalence in the presence of unit type ATTAPL: 6.1-6.3 HW #2 Out
Jan 25 The path-of-least-resistance approach to programming language theory, or: How to invent an algorithm by proving it correct before you know what it is; Monotonicity and Kripke logical relations ATTAPL: 6.4-6.8
Jan 30 Correctness of the extensional equivalence algorithm (continued) ATTAPL: Section 6.9 HW #2 Due
Feb 1 Review of HW #2; System F (predicative vs. impredicative polymorphism) Girard: Chapter 11; TAPL: Chapter 23 HW #3 Out
Feb 6 Termination for call-by-value System F (Girard's method)
Feb 8 Strong normalization for System F with full reduction; The method of candidate sets Girard: Chapter 14; Barendregt: 65-66 HW #3 Due
Feb 13 Review of HW #3; Strong normalization for System F (continued)
Feb 15 Simple set-based parametricity results; Breaking normalization via the inclusion of a non-parametric operation (Girard's J operator and the Harper-Mitchell variant J') Harper-Mitchell HW #4 Out
Feb 20 Reynolds' relational parametricity Reynolds
Feb 22 Wadler's "free theorems" Wadler
Feb 27 Operational notions of program equivalence: Kleene, contextual, ciu ATTAPL: 7.1-7.5; Harper: Chapter 27 HW #4 Due
Mar 1 Review of HW #4; Logical relations for contextual equivalence: Admissibility and TT-closure (Pitts' method) ATTAPL: 7.6
Mar 6 Pitts' method (continued)
Mar 8 Representation independence and extensionality principles; Directions for further study ATTAPL: 7.7