For detailed information about this course, please go to the course's page.

This course presents the principles, formalisms, and mathematical techniques that underlie many of today's typed programming languages, including OCaml, Haskell, and Rust.

Two written exams (a mid-term exam and a final exam) and one programming project are used to grade students.

Only printed course notes and hand-written notes are allowed during the written exams. Electronic devices are not allowed.

The course cannot be split.

A taste for programming is recommended.

Elementary knowledge of a functional programming language, such as Haskell or OCaml, is desirable.

Elementary knowledge of operational semantics (rewriting rules, inference rules) and of the lambda-calculus is useful, but not mandatory.

Some familiarity with the Coq proof assistant is useful, but not mandatory.

The course material (slides; programming project assignment; exam assignments and solutions; etc.) is written in English.

The lectures are by default taught in French, but are taught in English if at least one student requests it.

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