Last update: 18 avril 2013

MPRI course 2-4
Type systems

Didier Rémy

Year 2012-2013

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 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 on Tuesday at Chevaleret, in room 1E01 from 9:15 to 11:45

Program transformationsXavier LeroySep 18, 25; Oct 02, 09, 16
Type systemsDidier RémyOct 23, 30, Nov 06, 13; Dec 04, 11, 18
Subtyping and recursive typesGiuseppe CastagnaJan 08, 15, 22, 29
Towards proved programsYann Régis-GianasFev 05, 12, 19, 26
September      18        25     
October    02        09        16        23        30    
November    06         13         20         27     
December     04         11         18         25      
January     01         08         15         22         29    
February     05         12         19         26      
March     05         12      
Type systems

The whole course notes are available in this PDF that will be updated as we progress in the course. (You may see those of last year.)


The evaluation of the course is composed of a mid-term exam that on Tuesday December 04, a final exam on Tuesday March 12, 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

Here are the description and sources of this year programming task, The programming task must be returned by Friday, March 1st, 2013, at the lastest. (See the task description for how to submit.) For any question related to the programming task, contact Didier Remy or Yann Régis Gianas.

See below for additional information regarding the programming task.

List of changes to the sources

  1. Modified so that it is architecture independent.
  2. Modified rule App-Implicit and added a paragrah of explaination.