Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)

Responsable : Gilles Dowek


The course is in English (unless clearly only french speakers present)

Teaching in 2023 - 2024

Main Page of the Course


This course is about the notion of formal proof in mathematics and in informatics. It presents several logical formalisms, including type theories, focusing on the fact that they are meant to be used in proof systems such as Coq, Agda, HOL, Isabelle, PVS. We will treat in depth the articulation between reasoning and computation.

This course is a prerequisite / is linked to to the course Proof Assistants (2-7-2)

It is good to attend to both courses, although you are not required to.

We may to some lightweight exercises in Coq towards the end of the lessons in 2-7-1. Not so much to learn Coq, but in order to view the material in a different way. So it is a good idea to bring your computer with Coq installed (again see the instructions on the page of 2-7-2)

When and where ?

The lectures are on Mondays starting Sept. 18th, from 16:15-19:15, in the Sophie Germain Building, room 1004.


This is tentative

  1. Overview, First-Order Logic, Cuts
  2. Cuts in Arithmetic, constructivity
  3. Higher-Order Logic (HOL), inductive properties
  4. Functions in HOL
  5. Dependent Types, Curry-Howard, Cut Elimination
  6. Martin-Löf's Type Theory
  7. Impredicative Calculi
  8. To be decided


Written exam. Date TBA


Some familiarity with:

The notion of inductive definition.
The notions of free and bound variables, alphabetic equivalence, and substitution.
The syntax of (many-sorted) predicate logic.
The natural deduction.
The untyped lambda-calculus.
The simply typed lambda-calculus.
Rewrite rules.



Past exams


Gilles Dowek DR INRIA and ENS Paris-Saclay
Benjamin Werner PR Ecole polytechnique

Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA