MPRI course 2-4

Functional programming and type systems

Academic year 2012-2013

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:

• Didier Rémy's (Oct 23th-Dec 18th)
• Giuseppe Castagna's (Jan 8th-29th)
• Yann Régis-Gianas's (Feb 5th-26th)

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 (for parts 1, 2, 3 and some of part 4).

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).
Mid-term exam, with answers, for year 2011-2012 (covers X. Leroy's and D. Rémy's parts of the 2-4 course).