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 Transparents de l'exposé Éléments de bibliographie: Un article court et très accessible de Laurent Regnier, paru dans Quadrature en 2003 (Les limites de la correspondance de Curry-Howard) 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: Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970 (slides) Polymorphisme à tous les étages ! Du système F au calcul des constructions (slides) Mathématiques assistées par ordinateur, par Assia Mahboubi (optionnel mais intéressant) (slides)