MPRI

- Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)

Fondements des systemes de preuves / Foundations of proof systems (24h, 3 ECTS)

The topic of this course are the notions of formal proofs and of logical formalisms. The latter are considered through their possible implementation and use in proof systems (much as a programming language is implemented by a compiler).

We present several formalisms, including type theories used in several proof systems such as Coq, Agda, HOL, Isabelle, PVS. A particular point of attention will be the articulation between reasoning and computation.

When and where ?

The lectures are on Tuesdays from 16:15 to 19:30, in the Sophie Germain Building, room 1002. First course Sept. 14th

Schedule

Sept 14th : Motivations, aim (good formalisms), First-Order Logic & Natural deduction, Deduction Modulo, Logical Cuts.

slides (lecture 1)

Exam

Final Exam, length 2 hours. Date TBA

Prerequisites

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.