======  Intervention dans le séminaire interdisciplinaire Logique et Droit à l'IEP Paris ======
=== La démonstration à l’interface entre mathématiques, logique et informatique: Comprendre le comment du pourquoi ===

//**Séance du 27 janvier 2025**//
Séminaire organisé par Arnaud Durand.




**Plan de la séance:** 
  * Retour aux sources: l'origine de la démonstration en mathématiques et la constitution de la logique
  * Évolution des sytèmes de déduction: enrichir la structure des démonstrations
  * Quelques propriétés des déductions formelles
  * Logiques réalistes et déréalistes
  * Curry-Howard: entre preuves et programmes

**[[https://www.irif.fr/_media/users/saurin/teaching/iep/iepreuves.pdf|Transparents de l'exposé]]**


**Éléments de bibliographie:** 
  * [[https://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/ch.pdf|Un article court et très accessible de Laurent Regnier, paru dans Quadrature en 2003 (Les limites de la correspondance de Curry-Howard)]]
  * [[https://girard.perso.math.cnrs.fr/bordeaux.pdf|Texte introductif de Jean-Yves Girard, paru dans les leçons de mathématiques d'aujourd'hui (date de 1997): "La théorie de la démonstration, du programme de Hilbert à la logique linéaire"]] (environ 45 pages mais très lisibles)
  * Série de 2/3 leçons du cours de Xavier Leroy au Collège de France, slides et vidéos disponibles: 
  - [[https://www.college-de-france.fr/fr/agenda/cours/programmer-demontrer-la-correspondance-de-curry-howard-aujourd-hui/les-chemins-une-decouverte-la-correspondance-de-curry-howard-1930-1970|Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970]]  [[https://www.college-de-france.fr/sites/default/files/documents/xavier-leroy/UPL8552973399778523601_1.pdf|(slides)]]
  - [[https://www.college-de-france.fr/fr/agenda/cours/programmer-demontrer-la-correspondance-de-curry-howard-aujourd-hui/polymorphisme-tous-les-etages-du-systeme-f-au-calcul-des-constructions|Polymorphisme à tous les étages ! Du système F au calcul des constructions]] [[https://www.college-de-france.fr/sites/default/files/documents/xavier-leroy/UPL5826010689546642983_1b.pdf|(slides)]]
  - [[https://www.college-de-france.fr/fr/agenda/seminaire/programmer-demontrer-la-correspondance-de-curry-howard-aujourd-hui/mathematiques-assistees-par-ordinateur
|Mathématiques assistées par ordinateur, par Assia Mahboubi (optionnel mais intéressant)]] [[https://www.college-de-france.fr/sites/default/files/documents/xavier-leroy/UPL8901209141950115416_Mahboubi_2018_12_05.pdf|(slides)]]