The Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.

PropertyValue
dbpedia-owl:thumbnail
dbpprop:abstract
  • The Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.
  • La correspondance de Curry-Howard, appelée également correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité établissant une relation entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958 date à laquelle Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969 où William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul typé. La correspondance de Curry-Howard a joué un rôle important en logique, car elle a établi un pont entre théorie de la démonstration et informatique théorique. On la retrouve utilisée sous une forme ou une autre dans de très nombreux travaux allant des années 60 à nos jours : sémantique dénotationnelle, logique linéaire, réalisabilité, démonstration automatique...
  • Izomorfizm Curry'ego-Howarda jest to określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych systemów dowodzenia twierdzeń opartych na logice intuicjonistycznej, takich, jak np. Coq.
  • O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e demonstrações matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência demonstrações-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard.
  • Curry-Howard 对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做 Curry-Howard 同构或公式为类型对应。已经采用了一些不同的公式化，它的原理现在被认为是由美国数学家 Haskell Curry 和逻辑学家 William Alvin Howard 独立发现的。
dbpprop:reference
dbpprop:wikiPageUsesTemplate
dbpprop:wikibooksProperty
  • Haskell
  • The Curry-Howard isomorphism
rdfs:comment
  • The Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.
  • La correspondance de Curry-Howard, appelée également correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité établissant une relation entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul.
  • Izomorfizm Curry'ego-Howarda jest to określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych systemów dowodzenia twierdzeń opartych na logice intuicjonistycznej, takich, jak np. Coq.
  • O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e demonstrações matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência demonstrações-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard.
  • Curry-Howard 对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做 Curry-Howard 同构或公式为类型对应。已经采用了一些不同的公式化，它的原理现在被认为是由美国数学家 Haskell Curry 和逻辑学家 William Alvin Howard 独立发现的。
rdfs:label
  • Curry–Howard correspondence
  • Correspondance de Curry-Howard
  • Izomorfizm Curry'ego-Howarda
  • Isomorfismo de Curry-Howard
  • 柯里-霍华德同构
skos:subject
foaf:depiction
foaf:page
is dbpprop:redirect of