Last update: 22 juillet 2014

MPRI course 2-4
Type systems

Didier Rémy

Year 2013-2014

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 with also the help of
François Pottier.


This course was taught in 2012, 2011, and 2010, which was itself 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 (2012-2013)

The lessons will take place at University of Paris 7 - Denis Diderot, Batiment Sophie Germain from 9:15 to 11:45.

Program transformationsXavier LeroySep 17; Oct 01, 08, 15, 22
Type systemsDidier RémyOct 29, Nov 05, 12, 19, 26; Dec 10, 17
Subtyping and recursive typesGiuseppe CastagnaJan 07, 14, 21, 28
Towards proved programsYann Régis-GianasFev 04, 11, 18, 25

Type systems

The whole course are available in this PDF, which may be updated as we progress in the course.

If you don’t see the latest version, you may need to flush your browser cache to force realoading.

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


The evaluation of the course is composed of a mid-term exam that on Tuesday December 03, a final exam on Tuesday March 11, and a mandatory programming project, to be return by the end of February.

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

Paper course notes are allowed during written exams, but all electronic devices are forbidden.

Programming project

New: This year the programming project can also be done as pair-work (in teams of two people)—see the task description for details.

The programming task description is now available at To retreive it, type in a terminal:

        git clone

We recommend that you keep the git structure, so that in case we submit a new version with some modifications/corrections, they can be merged automatically into your working repository by just pulling them at the above address. The taks description alone can be accessed directly.

The programming task must be returned by Sunday, March 16th, 2014, at the lastest Instructions on how to submit are given in the task description. For any question related to the programming task, contact Yann Régis Gianas and Didier Remy.

Proposition de stage