- Présentation
- Procédures administratives
- Formation doctorale
- Appels d'offres
- Espace Doctorants
L'isomorphisme de Curry-Howard
Par Federico Olimpieri
L'isomorphisme de Curry-Howard indique que les preuves sont des programmes et que les propositions sont des types, c'est-à-dire des spécifications de programmes.
Cette correspondance apporte de nouvelles idées à la compréhension des deux notions de preuve mathématique et de calcul. En même temps, elle produit des applications remarquables dans les domaines de la logique et de l'informatique théorique.