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.
This course was taught in 2013, 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.
The lessons will take place at University of Paris 7 - Denis Diderot, Batiment Sophie Germain in room 1009 from 13:00 to 15:30.
Cours Teacher Program transformations Xavier Leroy Type systems Didier Rémy Towards proved programs Yann Régis-Gianas Towards mechanized meta-theory of programming languages Xavier Leroy
September 19 26 October 03 10 17 24 31 November 07 14 21 28 December 05 12 19 26 January 02 09 16 23 30 February 06 13 20 27 March 13
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.
The evaluation of the course is composed of a mid-term exam (on Friday, December 05), a final exam on Friday, March 13, 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.
The programming task description is now available. It should be returned by the end of February. See the instructions there.