Intervention dans le séminaire interdisciplinaire Logique et Droit à l'IEP Paris

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:

1. Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970 (slides)
2. Polymorphisme à tous les étages ! Du système F au calcul des constructions (slides)
3. Mathématiques assistées par ordinateur, par Assia Mahboubi (optionnel mais intéressant) (slides)