MPRI course 2-4
Type systems

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.

Note

This course was taught for the first time in 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 (2011-2012)

The lessons will take place on Tuesday at Chevaleret, room 1E01 from 9:15 to 11:45.

Cours	Teacher	Lessons
Program transformations	Xavier Leroy	Sep 13, 20, 27; Oct 04, 11
Type systems	Didier Rémy	Oct 18, 25; Nov 01, 08, 15; Dec 06, 13
Towards proved programs	Yann Régis-Gianas	Jan 03, 10, 17, 24
Subtyping and recursive types	Giuseppe Castagna	Jan 31; Fev 07, 14, 21

September		13	20	27
October	04	11	18	25
November	01	08	15	22	29
December	06	13	20	27
January	03	10	17	24	31
February	07	14	21	28
March	06

Type systems

Course notes are available in [PDF], which will 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 cours notes for each chapter below.

• Lesson 1, Oct 18: Simply typed lambda-calculus
• Lesson 2, Oct 25: Polymorphic lambda-calculus
• Lesson 3, Nov 08: Type reconstruction for simple types
• Lesson 4, Nov 15: Existential types and closure conversion (mutually recursive functions excluded)
• Lesson 5, Nov 22: Type reconstruction for core ML (type annotations, recursive types, and HM(X) excluded)
• Lesson 6, Dec 06: Overloading
• Lesson 7, Dec 13: Overloading (Type inference)

NB: The dates are exact, but the progression is approximate.

Evaluation

The evaluation of the course is composed of a mid-term exam that (on Tuesday 29, November 2011), a final exam (on Tuesday 28, February 2012 or Tuesday 6, March 2012), and a programming project which is mandatory.

• 2011-2012 mid-term exam: Parametricity     (subject and solutions)
• 2010-2011 final exam: Compiling a language with subtyping     (subject and solutions)
• 2010-2011 mid-term exam: Compilation of polymorphic records     (subject and solutions)

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

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

See there for the description and sources of this year programming task, to be returned by Friday 25, February 2012, at the lastest.