The course is in English

Benjamin Werner and Dominik Kirst

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

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

We may to some lightweight exercises in Rocq towards the end of the lessons. Not so much to learn Rocq, but in order to view the material in a different way. So it is a good idea to bring your computer with Rocq installed.

The lectures are on Fridays starting Sept. 18th, from 12:45-15:55, in the Sophie Germain Building, room 1009.

This is tentative

1. Overview, First-Order Logic, Strong Normalization of simple Types
2. Deduction modulo, Cuts in Arithmetic, Cut Elimination, Constructivity

TBA

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.