MPRI course 2-4
Type systems

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 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.

Plan for 2013-2014

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

Calendar

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	28
March	04	11

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.

• Lesson 1, Oct 24, Oct 31: Simply typed lambda-calculus
• Lesson 2, Oct 31, Nov 07: Polymorphic lambda-calculus
• Lesson 3, Nov 14, Nov 21: Type reconstruction for simple types
• Lesson 4, Nov 21, Dec 05: Existential types and closure conversion
• Lesson 5, Dec 05, Dec 12: Logical relations and parametricity
• Lesson 6, Dec 12, Jan 05: Overloading and type classes

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 05), a final exam , 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.)

• 2014-2015 mid-term exam: Information flow     (subject and solutions)
• 2013-2014 final exam: Operation on records     (subject and solutions)
• 2013-2014 mid-term exam: Typechecking Effects     (subject and solutions)
• 2012-2013 final exam: Refinement types     (subject and solutions)
• 2012-2013 mid-term exam: Variations on ML     (subject and solutions)
• 2011-2012 final exam: Intersection types     (subject and solutions)
• 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 exams of earlier years.

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

The programming task description will be available on December 10 and will have to be returned by the end of February.