Curry-Howard Isomorphism

A Curry-Howard Isomorphism is a isomorphism between formal logic systems (from proof theory) and computational calculi (from type theory).

• AKA: Curry–Howard Correspondence.
• See: Programming Language Theory, Proof Theory, Computer Program, Mathematical Proof, Haskell Curry, William Alvin Howard, L. E. J. Brouwer, Arend Heyting, Andrey Kolmogorov, Functional Programming Language.

---

---

References

2015

• (Wadler, 2015) ⇒ Philip Wadler. (2015). “Propositions As Types.” In: Communications of the ACM Journal, 58(12). doi:10.1145/2699407
  • QUOTE: Propositions as Types is a notion with many names and many origins. It is closely related to the BHK Interpretation, a view of logic developed by the intuitionists Brouwer, Heyting, and Kolmogorov in the 1930s. It is often referred to as the Curry–Howard Isomorphism, referring to a correspondence observed by Curry in 1934 and refined by Howard in 1969. Others draw attention to significant contributions from de Bruijn's Automath and Martin-Löf's Type Theory in the 1970s.

2014

• (Wikipedia, 2014) ⇒ http://en.wikipedia.org/wiki/Curry–Howard_correspondence Retrieved:2014-8-9.
  • In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs. It is a 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. It is the link between logic and computation that is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L. E. J. Brouwer, Arend Heyting and Andrey Kolmogorov.

1998

• (Sørensen & Urzyczyn, 1998) ⇒ Morten Heine Sørensen, and Pawel Urzyczyn. Technical Report TOPPS D-368. University of Copenhagen.
  • ABSTRACT: The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc. But there is much more to the isomorphism than this. For instance, it is an old idea --- due to Brouwer, Kolmogorov, and Heyting, and later formalized by Kleene's realizability interpretation --- that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. These notes give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism.

---