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.

Teaching in 2020-2021


This course focuses on the notion of formal proof in mathematics and in informatics. It presents several logical theories, including type theories used in several proof systems such as Coq, Agda, HOL, Isabelle, PVS. In particular we will treat in depth the articulation between reasoning and computation.

When and where ?

The lectures are on Wednesdays from 16:15 to 19:30, in the Sophie Germain Building, room 1013.


Wednesday, September 23th: Natural deduction - The notion of theory.
Wednesday, September 30th: The notion of model - Exercises.
Wednesday, October 7th: Arithmetic - Naive set theory.
Wednesday, October 14th: Simple type theory - Exercises.
Wednesday, October 21st: The termination of proof reduction.
Wednesday, October 28th: Dependent types - Exercises.
Wednesday, November 4th: Inductive types - Polymorphism.
Wednesday, November 18th: Master class - Preparation of the exam.
Warning: no lecture on Wednesday, September 16th and on Wednesday, November 11th.


Wednesday, December 2nd, 16h15-18h15, room 1013. Course notes and personal documents allowed.


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.
The expression of computable functions in arithmetic, in the language of rewrite rules and in the lambda-calculus.



Past exams


Gilles Dowek DR INRIA and ENS Paris-Saclay
Benjamin Werner PR Ecole polytechnique
Pierre-Yves Strub MdC 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