Responsable : Benjamin Werner, Gilles Dowek

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

Benjamin Werner

here

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 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)

The lectures are on Tuesdays starting Sept. 17th, from 16:15-19:15, in the Sophie Germain Building, room 1002.

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.