__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.