Functional programming and type systems

Metatheory

This is the course material on the Metatheory of Type Programming Languages part of the course 2-4 of the MPRI that I taught between 2010 and 2023.

The course has evolved over time with a significant change in 2016. Some lessons have not been taught after 2016 or taught differently by other colleagues. This is the union of all lectures given over this period. Hence, some lectures come in several versions: for instance, Simply-typed lambda-calculus and System F were first taught in separate lectures, including detailed proofs, as in the course notes, but were later taught in a single lecture Metatheory of System F, leaving out the proofs. Similarly, effects were first presented in the lecture on system F, and them presented in a separate lecture. We keep all lectures below, hence with some overlapping:

• Simply-typed lambda-calculus     [slides] [handout]
• System F     [slides] [handout]
• Meta-theory of System F [slides] [handout]
• Data-types, existential types, GADTs     [slides] [handout]
• Fomega: higher-kinds and higher-order types     [slides] [handout]
• Logical relations and parametricity     [slides] [handout]
• Effects: References, exceptions, and value restriction [slides] [handout]
• Type reconstruction     [slides] [handout]
• Overloading     [slides] [handout]

The course notes area also available as a single file [Slides] [handout].