Preuves et programmes : Outils classiques
8 ECTS, semestre 2, 12 semaines
| Validation | CC+examen |
| Enseignant | Guillaume Geoffroy et Hugo Herbelin |
| Horaires hebdomadaires | 4.0 h CM |
| Années | Master Logique Mathématique et Fondements de l'Informatique M2 Logos |
Syllabus
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.
Sommaire
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 implicative et leur complétude vis-à-vis des tripos.