Ecole Doctorale 184

Ceci est une ancienne révision du document !

---

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.