Preuves-programmes : outils classiques

Code APOGÉE : MA2DE010 | 6 ECTS | Enseignants : Guillaume Geoffroy et Hugo Herbelin | Validation : CC + examen
Horaires hebdomadaires : 4h CM | Mutualisé avec : M2 LMFI

Ce cours portera sur le contenu calculatoire des preuves, aussi bien en logique constructive qu’en logique classique et en présence de principes de choix comme la bar-induction.

Programme

Le cours comportera deux parties :

I – La correspondance de Curry-Howard-Lambek

Du triangle lambda-calcul simplement typé/calcul propositionnel intuitionniste/catégories cartésiennes closes au triangle F-omega/HOL/topos élémentaires et à la théorie des types de Martin-Löf, en passant par le système F ; d’abord dans un cadre intuitionniste, puis extension à la logique classique. Correspondance indexé/fibré.

II – La réalisabilité

Réalisabilité de Kleene, de Kreisel, interprétation Dialectica de Gödel, réalisabilité de Krivine en logique classique ; étude fine de la logique induite par chacun de ces systèmes. Liens avec le forcing. Tripos et topos de réalisabilité, algèbres implicatives et leur complétude vis-à-vis des tripos.