Last update: 31 janvier 2011

MPRI course 2-4
Type systems

Didier Rémy

Year 2010-2011

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.


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.

Type systemsDidier RémySep 14, 21, 28; Oct 05, 12, 19, 26
Towards proved programsYann Régis-GianasNov 02, 09, 16, Dec 7
Subtyping and recursive typesBeppe CastagnaDec 14; Jan 04, 11, 18
Program transformationsXavier LeroyFev 01, 08, 15, 22; Mar 01
Type systems


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.

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

Programming project

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