Théorie de la démonstration
Cours de recherche (30h de cours, travail
sur des articles scientifiques)
Cours : Philippe Audebaud,Tom Hirschowitz (Philippe.Audebaud, Tom.Hirschowitz)
La logique mathématique étudie la validité des
formules sous certaines hypothèses. La théorie de la démonstration
raffine la logique en prenant au sérieux l'identité des
démonstrations: quand doit-on considérer que deux démonstrations
d'une même formule sont équivalentes? Une découverte majeure de la
théorie de la démonstration est la correspondance de Curry-Howard,
qui relie la question de l'identité des démonstrations à la théorie
des langages de programmation. Depuis cette découverte, la
correspondance a été et est encore étendue à de nouveaux cadres
logiques et à de nouveaux langages de programmation. Le cours
survole ce domaine de recherche, de la relation entre logiques
propositionnelles intuitionniste et classique basée sur les
traductions par passage de continuations, jusqu'aux interprétations
calculatoires des quantificateurs et leurs sémantiques
dénotationnelles. Voir le résumé en anglais pour une esquisse
du contenu.
Bibliographie
Pour éviter de submerger l'étudiant intéressé, on
donne juste quelques grands classiques:
-
Dowek. Théorie des types. Cours de
M2. .
- Girard, Lafont, Taylor. Proofs and Types. Cambridge
University Press, 1989.
- Krivine. Lambda-calcul, types et modèles. Masson, 1990.