MPRI course 2-4
Type systems

This is the location for the course material for the first 7 lessons of the course 2-4 of the MPRI.
The other lessons are taught by Yann Régis-Gianas, Giuseppe Castagna, and Xavier Leroy.
The programming task will be organized by François Pottier.

Note

This is a reorganization of the course of the same name that was taught the previous years. You may find the old course notes of François Pottier on type systems, or my previous course notes on modularity.

Plan (2010-2011)

The lessons will take place on Tuesday at Chevaleret, room 0D4 from 13:15 to 15:45.

Cours	Teacher	Lessons
Type systems	Didier Rémy	Sep 14, 21, 28; Oct 05, 12, 19, 26
Towards proved programs	Yann Régis-Gianas	Nov 02, 09, 16, Dec 7
Subtyping and recursive types	Beppe Castagna	Dec 14; Jan 04, 11, 18
Program transformations	Xavier Leroy	Fev 01, 08, 15, 22; Mar 01

Type systems

• Lesson 1, Sep 14: Simply typed lambda-calculus
• Lesson 2, Sep 21: Polymorphic lambda-calculus
• Lesson 3, Sep 28: Type reconstruction (Core language)
• Lesson 4, Oct 05: Type reconstruction (Language extensions)
• Lesson 5, Oct 12: Existential types and closure conversion (updated Nov 4)
• Lesson 6, Oct 19: Overloading
• Lesson 7, Oct 26: Overloading (Type inference)

Evaluation

The evaluation of the course is composed of a mid-term exam that (on Tuesday November 23), a final exam (on Tuesday March 1 or 8), and a programming project which is mandatory.

• mid-term exam 2010-2011, Subject and solutions of : compilation of polymorphic records

Although the content of the course has changed, you may still see previous years exams.

Here are the description and source code of this year programming task. The programming task must be returned by Friday, February 25 at the lastest (see the task description for how to submit).