Typed Operational Reasoning (Winter 2008)

Course Information

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

Description

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%)

Lectures

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]

Likely Topics for the Coming Lectures

References

  1. Benjamin C. Pierce. Types and Programming Languages, MIT Press, 2002.
  2. Henk Barendregt. Lambda calculi with types. Handbook of Logic in Computer Science, Volume 2, 1992.
  3. Jean-Yves Girard. Proofs and Types. Translated and with appendices by Paul Taylor and Yves Lafont, Cambridge University Press, 1990.
  4. Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages, MIT Press, 2005.
  5. Christopher A. Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In POPL 2000.
  6. Christopher A. Stone and Robert Harper. Extensional equivalence and singleton types. ACM Transactions on Computational Logic, 7(4):676-722, October 2006.
  7. Jean Gallier. On Girard's "Candidats de Reductibilité". In Logic and Computer Science, Odifreddi, editor, Academic Press, 123-203, 1990.
  8. Robert Harper and John C. Mitchell. Parametricity and variants of Girard's J operator. Information Processing Letters, 1999.
  9. Imre Lakatos. Proofs and Refutations: The Logic of Mathematical Discovery, Cambridge University Press, 1976.
  10. John C. Reynolds. Types, abstraction and parametric polymorphism. Information Processing 1983.
  11. Philip Wadler. Theorems for free! In FPCA 1989.
  12. Andrew J. Kennedy. Relational parametricity and units of measure. In POPL 1997.
Imprint / Data Protection
Last modified: February 14 2020 11:48:02