This is the material for X. Leroy's lectures in the MPRI 2-4 course (Sept 19th to Oct 17nd). 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.
Further reading: (optional)
Download (version 1.2) as a tar.gz archive or a zip archive.
This year's programming project is about nondeterministic and probabilistic functional programming using monads. The archives above contain the description of the tasks, plus some OCaml sources provided as starting points.
Deadline for submitting solutions: Sunday, 1 March 2015, 23:59
src/Typing.ml. Added a test case in
src/Mlist.mlto check recursive memoization.
src/Nondet.mland bugs in
src/Testmemo.ml. The task description is unchanged.