MPRI course 2-4

Functional programming and type systems

Academic year 2011-2012

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

• Didier Rémy's (Oct 18th-Dec 13th)
• Yann Régis-Gianas's (Jan 3rd-Jan 24th)
• Giuseppe Castagna's (Jan 31st-Feb 21st).

Program execution and transformations:

Slides for the lectures:

• Part I: interpreters and operational semantics
• Part II: abstract machines and compilation
• Part III: program transformations
• Part IV: monads, with accompanying Caml code.
• Part V: functional intermediate representations.

Exercises and some answers.

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 from the APPSEM 2000 school: Monads and Effects by N. Benton, J. Hughes, and E. Moggi.

Final exam, with answers, for year 2010-2011 (covers G. Castagna's and X. Leroy's parts of the 2-4 course).

Programming project:

• The description of the tasks (version 1.0)
• The sources provided as starting point (version 1.0).

Deadline for submitting solutions: Monday, 27 February 2012, 9:00 AM

Change log:

• 2011-11-09: initial release (version 1.0)