Last update: 26 novembre 2023

## Functional programming and type systems |

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].