MPRI course 2-4

Functional programming and type systems

Academic year 2016-2017

This is the material for X. Leroy's lectures in the MPRI 2-4 course (Sept 16th to Oct 14th). Click on the following links for the other lectures:

• Didier Rémy
• Yann Régis-Gianas

Outline for the whole course.

Program execution and transformations:

Slides for the lectures:

• Part I: interpreters and operational semantics: for viewing and for printing.
• Part II: abstract machines and compilation: for viewing and for printing.
• Part III: program transformations: for viewing and for printing.
• Part IV: monads: for viewing and for printing, with accompanying Caml code.
• Part V: functional intermediate representations: for viewing and for printing.
• Part VI: towards Coq mechanization: for viewing, with accompanying Coq development:
  • 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.
  An archive of the Coq sources (Coq 8.5 or 8.6).

Exercises and some answers. (Updated every week.)

Further reading: (optional)

• Basic notions on the untyped lambda-calculus and de Bruijn's nameless notation: chapters 5, 6 and 7 of Types and Programming Languages by B. C. Pierce.
• More details on inductive and coinductive semantics, on the Modern SECD machine, and on its correctness proofs: Coinductive big-step operational semantics by X. Leroy and H. Grall.
• Course notes on monads: Monads and Effects by N. Benton, J. Hughes, and E. Moggi.