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!
|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|