MPRI 2-7-1
Foundations of
Proof-Systems
Fondements des
Systemes de Preuves
Cours 2-7-1 du MPRI
2012-2013
This year, the course
is given by Benjamin Werner.
The course's
page on the MPRI site.
On mondays, 16:15 -
19:15, salle 1E20, 175 rue du Chevaleret / 16 rue Clisson, 75013 Paris.
Temptative Schedule
- 24/09 Introduction, motivations.
First-Order Logic, intuitionistic natural deduction, cuts,
computational content.
- 01/10 Cuts in arithmetic,
axiomatic cuts, deduction modulo. Naive set theory.
- 08/10 Simply-Typed
lambda-calculus, strong normalization, Church's higher-Order Logic
(HOL)
- 15/10 Function definitions in
HOL. Godel's system T.
- 22/10 Curry-Howard isomorphism.
- 29/10 or 5/11 Martin-Lof's Type
Theory.
- 12/11 Impredicativity, system F,
the Calculus of Constructions, Barendergt's Cube.
- 19/11 Impredicativity + Exercices, revision...
- 26/11 (confirmed) exam
Course Notes
The course notes of Gilles
Dowek give a good account (that is a correct and complete account)
of what I will present. You can use french and english versions of these
notes. There are some differences in the presentation of the material
between these versions, but both are usable.
I made pdf files : french
and english.
The original files are on Gilles' page.
Other material
Some videos(en francais)
