Curry–Howard correspondence

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. At the ver... more

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. At the very beginning, the Curry–Howard correspondence is In other words, the Curry–Howard correspondence is the simple observation that two at-the-time-seemingly-unrelated families of formalisms, the proof systems on one side and the models of computation on the other side, were, on the two examples considered by Curry and Howard, in fact structurally the same kind of objects. If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type... less