Last update: 13 juillet 2017

MPRI course 2-4
Type systems

Didier Rémy

Year 2015-2016

This is the location for the course material on the Type systems part of the course 2-4 of the MPRI.
The other lessons are taught by
Xavier Leroy and Yann Régis-Gianas.

Note

This course has been taught yearly since 2010 (here is the 2015 session). You may also read the old course notes of François Pottier on type systems and my previous course notes on modularity.

Plan for 2015-2016

The lessons will take place at University of Paris 7 - Denis Diderot, Batiment Sophie Germain in room SG2 (to be confirmed) at 12:45. The lessons lasts 2:30, except the lessons of Didier Rémy, which will last 2:45 to compensable for the November 11 holiday.

CoursTeacher
Program transformationsXavier Leroy
Type systemsDidier Rémy
Towards proved programsYann Régis-Gianas
Towards mechanized meta-theory of programming languagesXavier Leroy

Calendar

September 
    16    
    23    
    30    
 
October
    07    
    14    
    21    
    28    
 
November
    04    
    11    
    18    
    25    
 
December
    02    
    09    
    16    
    24    
    31    
January
    06    
    13    
    20    
    27    
 
February
    03    
    10    
    17    
    24    
 
March
    03    
    10    
 

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.

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

Evaluation

The evaluation of the course is composed of a mid-term exam on Friday, December 04, a final exam on Friday, March 11, and a mandatory programming project, to be returned by the end of February. (Course notes and hand-written notes are allowed for the exams, but computers or other electronic devices are not.)

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

The programming task description will be released before Xmas vacations, and will be due before by the last lesson on February 24th.