Curry–Howard correspondence

In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.

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 the 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 (see Brouwer–Heyting–Kolmogorov interpretation) and Stephen Kleene (see Realizability). The relationship has been extended to include category theory as the three-way Curry–Howard–Lambek correspondence.

Origin, scope, and consequences

The beginnings of the Curry–Howard correspondence lie in several observations:

In 1934, Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.

In 1958, he observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment with the typed fragment of a standard model of computation known as combinatory logic.

In 1969 Howard observes that another, more "high-level" proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus.

Actually, Howard's first formulation of the isomorphism was referred to (a variant of) Gentzen's sequent calculus. The observation that the isomorphism is best understood with natural deduction, as well as the current formulation of the isomorphism itself, are due to Per Martin-Löf.