MPRI course 2-4
Functional programming and type systems
Metatheory of System F

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 gitlab page

https://gitlab.inria.fr/fpottier/mpri-2.4-public/blob/master/README.md

Note

A previous version of this course has been taught yearly since 2010 (see the 2016 session), but this year sessions has changed significantly.

Plan for 2017-2018

The lessons will take place at University of Paris 7 - Denis Diderot, Batiment Sophie Germain in room SG1 (2035) at 12:45. The lessons lasts 2:30.

Cours	Teacher
Functional Programming: Under the hood	François Pottier
Metatheory of Typed Programming Languages	Didier Rémy
Advanced Aspects of Type Systems	Yann Régis-Gianas
Dependentlty-typed Functional Programming	Pierre-Évariste Dadang

Calendar

September		15	22	39
October	06	13     A	20	27
November	03	10     +	17	24
December	01	08	15	22	29
January	05	12	19	26
February	02	09	16	23
March	02	09

Type systems

The course notes will be available here when the course begins. Meanwhile, you may see those of last year.

You may also retreive the course notes for each chapter below.

• Lesson 1, Sep 15: System F (See also lessons 1 and 2 of previous year)
• Lesson 2, Oct 27: Data-types, existential types, GADTs
• Lesson 4, Nov 03: Logical relations and parametricity
• Lesson 3, Nov 10: Subtyping. Row Polymorphism
• Lesson 5, Nov 17: References. Value restriction Logical relations and parametricity

NB: The dates are exact, but the progression is approximate. Course notes may be modified before each lesson.