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 2018-2019

Course Page


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 each Tuesday from 8:45 to 12:00, in the Sophie Germain Building, room 1013


September 10th: Inductive definitions. Natural deduction
September 17th: Logical and axiomatic cuts - Arithmetic
September 24th: Normalization of simply typed lambda-calculus and System T
October 1st: Higher-Order Logic


Tuesday, Nov. 19th 2019, 9h-11h30, 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

Internships (last year - to be updated)

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