Outils pour utilisateurs

Outils du site


espace_doctorants:seminaire:l_isomorphisme_de_curry-howard

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

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.
espace_doctorants/seminaire/l_isomorphisme_de_curry-howard.1519312416.txt.gz · Dernière modification: 2018/02/22 16:13 par guillaume.geoffroy