Last update: 2 octobre 2019
The location for the course material on the Metatheory of Type
Programming Languages part of the course 2-4 of the
MPRI is now at the
A previous version of this course has been taught yearly since
2010 (see also the 2016 session), but the course
has changed significantly since 2017.
- (21/10/2020) Metatheory of System F (handout) (see also intro, and chap 1,2,3 and 4 of course notes)
- (28/10/2020) ADTs, existential types, GADTs (handout without or only the extra material) (see also chap 6 of course notes)
- (04/11/2020) References, Value restriction, Side effects (handout) (see also sections 3.6, 3.7 and 4.5 of course notes)
- No lecture on 11/11/2020.
- (18/11/2020) This slot will (most likely) be used to finish and/or revised the material in the previous 3 lectures.
- (25/11/2020) A (slow) walk through the garden of type soundness proofs. In Coq, by François Pottier (coq, html). To view the proofs online, please use the following links:
- The mid-term exam takes place on 02/12/2020. (The correction is now avaliable below)
- (09/12/2020) Overloading (handout) (see also chap 7 of course notes)
- (16/12/2020) Logical relations (handout) (chap 8 of course notes)
- See exercises in course notes