Person in charge: Didier Rémy

The content for 2021-2022 has changed significantly.

• Interpretation, compilation, and program transformations (François Pottier)
• Metatheory of Typed Programming Languages (Didier Rémy)
• Effects (Gabriel Scherer)
• Dependently-typed Functional Programming (Pierre-Evariste Dagand)
• Rust: programming with ressources (Jacques-Henri Jourdan)

This course presents the principles and formalisms that underlie many of today's typed functional programming languages.

The course is made up of five parts and cannot be split.

Two written exams (a partial and a final exam) and one programming project or several programming exercises are used to evaluate the students that follow the full course. Only the partial exam will count to grade students who split the course.

Only course notes and hand written notes are allowed for the written exams.

Previous exams are available with solutions, but for a slightly different content of the course.

As part of this course, the students will be given an individual programming task or several programming exercises that will be used to illustrate, put into practice, or explore in detail one particular topic of the course. These will count for the evaluation of the students.

Elementary notions of operational semantics and lambda-calculus (rewriting rules, inference rules), and a taste for programming, particularly in OCaml.

The course notes are in English. The lectures are by default in French, but English will be used if French is a real problem for some students.

• Pierre-Evariste Dagand
• Jacques-Henri Jourdan
• François Pottier
• Didier Rémy
• Gabriel Scherer