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

### Language

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

### Objectives

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.

### Schedule

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

### Exam

Written exam. Date TBA

### Prerequisites

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.

### Team

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

Universités partenaires
Établissements associés