Ci-dessous, les différences entre deux révisions de la page.
espace_doctorants:seminaire:l_isomorphisme_de_curry-howard [2018/02/22 16:13] guillaume.geoffroy créée |
espace_doctorants:seminaire:l_isomorphisme_de_curry-howard [2018/02/22 16:17] (Version actuelle) guillaume.geoffroy |
||
---|---|---|---|
Ligne 1: | Ligne 1: | ||
__L'isomorphisme de Curry-Howard__ | __L'isomorphisme de Curry-Howard__ | ||
- | Par Federico Olimpieri | + | //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. | 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. | 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. |