Preuves Constructives
Les notes de Gilles Dowek en dvi
et ps zippé.
Les transparents d'introduction en dvi
animé et ps zippé. Idem pour le
premier cours: dvi
animé et ps zippé.
Pour voir les dvi bouger: advi.
Examens anciens
- L'énoncé de l'examen 2002 (ps, dvi) et son corrigé (ps, dvi)
- L'énoncé de l'examen 2001 (ps, dvi).
- L'énoncé de l'examen 2000 (ps, dvi) et son corrigé (ps, dvi)
- Dans ce répertoire, en vrac, les examens des années précédantes et
quelques corrigés.
Divers
- La construction du modèle ensembliste de la théorie de Martin-Löf
(et une définition précise de celle-ci par la même occasion); en ps et dvi.
- Pour les fanas de preuves de normalisation: le chapitre 3 de ma
thèse présente la méthode de réductibilité; on y trouve des preuves
pour les systèmes T et F; ps.
La partie sur les types dépendants est
définitivement hors-programme.