This is the material for X. Leroy's lectures in the MPRI 2-4 course (Sept 18th to Oct 16th). Click on the following links for the other lectures:
Outline for the whole course.
Slides for the lectures:
Sequences: library on transition sequences
Semantics: small-step and big-step semantics, equivalence proofs
Typing: simple types with subtyping; soundness proof
Compiler: compilation to the Modern SECD; compiler correctness proof.
CPS: CPS conversion.
Exercises and some answers. (Final update 2015-10-27 with all the answers.)
Further reading: (optional)
Download (version 1.1) as a tar.gz archive.
This year's programming project is the implementation (type-checking and compilation) of a simple functional language with records and subtyping. The archives above contain the description of the tasks, plus some OCaml sources provided as starting points.
Deadline for submitting solutions: Sunday, 28 February 2016, 23:59.