Parametricity and Modular Reasoning

Instructor: Derek Dreyer

Time: Tue, Thu @ 2-4 PM

Place: Campus E1.5, Room 029 (videocast to KL)

Abstract:

Abstract data types (ADTs) and other facilities for information hiding in programming languages (e.g. private fields, local variables) are widely considered to be crucial for supporting data abstraction and modularity, but what does that actually buy us in terms of reasoning about our code? As it turns out, it buys us a great deal, but formalizing what it buys us, especially in the context of modern programming languages, is quite tricky.

The formal essence of data abstraction was first characterized by John Reynolds in a landmark 1983 paper, "Types, Abstraction and Parametric Polymorphism", in which he introduced the concept of "relational parametricity" via his "abstraction theorem". The abstraction theorem formally establishes that the behavior of clients of an ADT must be unaffected by changes to the internal representation of the ADT that are preserved by its operations. However, Reynolds's original work only concerned pure System F, the polymorphic lambda-calculus, and there have since been decades of work on extending and generalizing his results to richer, more realistic languages supporting a host of computational effects.

In this course, we will start with Reynolds's work and build progressively toward semantic models of modern languages, such as Kripke logical relations and bisimulations models, which support very subtle and sophisticated forms of modular reasoning. To keep the formal material of the course in a unified framework, we will focus on models of data abstraction based on *operational* semantics, in the tradition of the work of Andrew Pitts.

As a basic prerequisite, students should be familiar with standard operational techniques, such as proofs by induction over operational semantics and type systems, which are covered in Pierce's TAPL book and Harper's PFPL book, among other sources. The grade will be based on homework assignments, student presentations on assigned papers, and class participation.

Along the way, we will explore a number of the following topics, possibly among others:

- Proving termination/normalization of System F (Girard's method, "unary logical relations")

- Relational parametricity (Reynolds's "binary logical relations")

- Using parametricity to show definability of types by Church encodings

- "Free" theorems (Wadler) and applications to fusion optimizations (Johann)

- Supporting recursion and context-sensitive semantics by "TT-closure" (Pitts)

- Supporting local invariants on first-order state via "Kripke logical relations" (Pitts-Stark)

- Supporting recursive types and higher-order state by "step-indexed" Kripke logical relations (Appel-McAllester, Ahmed)

- Transitional invariants (Dreyer et al.)

- Environmental bisimulations (Sumii et al.)

- Parametric bisimulations (Hur et al.)

- Logical relations for concurrency (Turon et al.)