Previous Up Next

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:
Previous Up Next