Cette année, le cours est assuré par Benjamin Werner; il sera suivi du cours 2-7-2 plus centré sur l’utilisation du système Coq.

This year,the course is given by Benjamin Werner; it will be followed by the course 2-7-2 which is more centered on the Coq proof system.

Forthcoming lectures:

1. *12 oct. Functions in HOL
   

2. *19 oct. Gödel’s System T
   

3. *26 oct. Curry-Howard isomorphism (1): λΠ-calculus
   

4. *2 nov. Curry-Howard isomorphism (2): Martin-Löf’s Type Theory
   

5. *9 nov. System F
   

6. *16 nov. Models
   

Liens :

1. *Examens anciens.
   

2. *Notes de cours de Gilles Dowek (français)
   

3. *Course Notes by Gilles Dowek (english)
   

4. *Coq
   

* TDs Coq par Sylvie Boldo et al.

Vidéos pour la culture générale :

1. *Gilles Dowek sur Diophante
   

2. *Gilles Kahn sur le calcul
   

3. *Benjamin Werner sur les preuves calculatoires