A proof written as a functional program
plus_comm=funnm:nat=>nat_ind(funn0:nat=>n0+m=m+n0)(plus_n_0m)(fun(y:nat)(H:y+m=m+y)=>eq_ind(S(m+y))(funn0:nat=>S(y+m)=n0)(f_equalSH)(m+Sy)(plus_n_Smmy))n:forallnm:nat,n+m=m+n
A proof of commutativity of addition on natural numbers in the proof assistantRocq (previously known asCoq).nat_ind stands formathematical induction,eq_ind for substitution of equals, andf_equal for taking the same function on both sides of the equality. Earlier theorems are referenced showing${\displaystyle m=m+0}$ and${\displaystyle S(m+y)=m+Sy}$.

Inprogramming language theory andproof theory, theCurry–Howard correspondence is the direct relationship betweencomputer programs andmathematical proofs. It is also known as theCurry–Howard isomorphism orequivalence, or theproofs-as-programs andpropositions- orformulae-as-types interpretation.

It is a generalization of a syntacticanalogy between systems of formal logic and computational calculi that was first discovered by the AmericanmathematicianHaskell Curry and thelogicianWilliam Alvin Howard.^[1] 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 ofintuitionistic logic given in various formulations byL. E. J. Brouwer,Arend Heyting andAndrey Kolmogorov (seeBrouwer–Heyting–Kolmogorov interpretation)^[2] andStephen Kleene (seeRealizability). The relationship has been extended to includecategory theory as the three-wayCurry–Howard–Lambek correspondence.^[3][4][5]

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

1. In 1934Curry observes that thetypes of the combinators could be seen asaxiom-schemes forintuitionistic implicational logic.^[6]
2. In 1958 he observes that a certain kind ofproof system, referred to asHilbert-style deduction systems, coincides on some fragment with the typed fragment of a standardmodel of computation known ascombinatory logic.^[7]
3. In 1969Howard observes that another, more "high-level"proof system, referred to asnatural deduction, can be directly interpreted in itsintuitionistic version as a typed variant of themodel of computation known aslambda calculus.^[8]

The Curry–Howard correspondence is the observation that there is an isomorphism between the proof systems, and the models of computation. It is the statement that these two families of formalisms can be considered as identical.

If one abstracts on the peculiarities of either formalism, the following generalization arises:a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as ananalogy that states that thereturn type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form oflogic programming on a rigorous foundation:proofs can be represented as programs, and especially as lambda terms, orproofs can berun.

The correspondence has been the starting point of a large range of new research after its discovery, leading to a new class offormal systems designed to act both as aproof system and as a typedprogramming language based onfunctional programming. This includesMartin-Löf'sintuitionistic type theory andCoquand'scalculus of constructions (CoC), two calculi in which proofs are regular objects of the discourse and in which one can state properties of proofs the same way as of any program. This field of research is usually referred to as moderntype theory.

Suchtyped lambda calculi derived from the Curry–Howard paradigm led to software like Rocq in which proofs seen as programs can be formalized, checked, and run.

A converse direction is touse a program to extract a proof, given itscorrectness—an area of research closely related toproof-carrying code. This is only feasible if theprogramming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry–Howard correspondence practically relevant.

The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts that were not covered by the original works of Curry and Howard. In particular,classical logic has been shown to correspond to the ability to manipulate thecontinuation of programs and the symmetry ofsequent calculus to express the duality between the twoevaluation strategies known as call-by-name and call-by-value.

Because of the possibility of writing non-terminating programs,Turing-complete models of computation (such as languages with arbitraryrecursive functions) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on usingmonads to segregate provably terminating from potentially non-terminating code (an approach that also generalizes to much richer models of computation,^[9] and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism^[10]). A more radical approach, advocated bytotal functional programming, is to eliminate unrestricted recursion (and forgoTuring completeness, although still retaining high computational complexity), using more controlledcorecursion wherever non-terminating behavior is actually desired.

In its more general formulation, the Curry–Howard correspondence is a correspondence between formalproof calculi andtype systems formodels of computation. In particular, it splits into two correspondences. One at the level offormulas andtypes that is independent of which particular proof system or model of computation is considered, and one at the level ofproofs andprograms which, this time, is specific to the particular choice of proof system and model of computation considered.

At the level of formulas and types, the correspondence says that implication behaves the same as a function type, conjunction as a "product" type (this may be called a tuple, a struct, a list, or some other term depending on the language), disjunction as a sum type (this type may be called a union), the false formula as the empty type and the true formula as a unit type (whose sole member is the null object). Quantifiers correspond todependent function space or products (as appropriate). This is summarized in the following table:

At the level of proof systems and models of computations, the correspondence mainly shows the identity of structure, first, between some particular formulations of systems known asHilbert-style deduction system andcombinatory logic, and, secondly, between some particular formulations of systems known asnatural deduction andlambda calculus.

Between the natural deduction system and the lambda calculus there are the following correspondences:

It was at the beginning a simple remark in Curry and Feys's 1958 book on combinatory logic: the simplest types for the basic combinators K and S ofcombinatory logic surprisingly corresponded to the respectiveaxiom schemesα → (β →α) and (α → (β →γ)) → ((α →β) → (α →γ)) used inHilbert-style deduction systems. For this reason, these schemes are now often called axioms K and S. Examples of programs seen as proofs in a Hilbert-style logic are givenbelow.

If one restricts to the implicational intuitionistic fragment, a simple way to formalize logic in Hilbert's style is as follows. Let Γ be a finite collection of formulas, considered as hypotheses. Then δ isderivable from Γ, denoted Γ ⊢ δ, in the following cases:

• δ is an hypothesis, i.e. it is a formula of Γ,
• δ is an instance of an axiom scheme; i.e., under the most common axiom system:
  • δ has the formα → (β →α), or
  • δ has the form (α → (β →γ)) → ((α →β) → (α →γ)),
• δ follows by deduction, i.e., for someα, bothα →δ andα are already derivable from Γ (this is the rule ofmodus ponens)

This can be formalized usinginference rules, as in the left column of the following table.

Typed combinatory logic can be formulated using a similar syntax: let Γ be a finite collection of variables, annotated with their types. A term T (also annotated with its type) will depend on these variables [Γ ⊢ T:δ] when:

• T is one of the variables in Γ,
• T is a basic combinator; i.e., under the most common combinator basis:
  • T is K:α → (β →α) [whereα andβ denote the types of its arguments], or
  • T is S:(α → (β →γ)) → ((α →β) → (α →γ)),
• T is the composition of two subterms which depend on the variables in Γ.

The generation rules defined here are given in the right-column below. Curry's remark simply states that both columns are in one-to-one correspondence. The restriction of the correspondence tointuitionistic logic means that someclassicaltautologies, such asPeirce's law ((α →β) →α) →α, are excluded from the correspondence.

Hilbert-style intuitionistic implicational logic	Typed combinatory logic
${\displaystyle \frac{\alpha \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢\alpha }\text{Assum}}$	${\displaystyle \frac{x:\alpha \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\alpha }}$
${\displaystyle \frac{}{\mathrm{\Gamma }⊢\alpha \to (\beta \to \alpha )}{\text{Ax}}_K}$	${\displaystyle \frac{}{\mathrm{\Gamma }⊢K:\alpha \to (\beta \to \alpha )}}$
${\displaystyle \frac{}{\mathrm{\Gamma }⊢(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))}{\text{Ax}}_S}$	${\displaystyle \frac{}{\mathrm{\Gamma }⊢S:(\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))}}$
${\displaystyle \frac{\mathrm{\Gamma }⊢\alpha \to \beta \mathrm{\Gamma }⊢\alpha }{\mathrm{\Gamma }⊢\beta }\text{Modus Ponens}}$	${\displaystyle \frac{\mathrm{\Gamma }⊢E_1:\alpha \to \beta \mathrm{\Gamma }⊢E_2:\alpha }{\mathrm{\Gamma }⊢E_1{E}_2:\beta }}$

Seen at a more abstract level, the correspondence can be restated as shown in the following table. Especially, thededuction theorem specific to Hilbert-style logic matches the process ofabstraction elimination of combinatory logic.

Thanks to the correspondence, results from combinatory logic can be transferred to Hilbert-style logic and vice versa. For instance, the notion ofreduction of terms in combinatory logic can be transferred to Hilbert-style logic and it provides a way to canonically transform proofs into other proofs of the same statement. One can also transfer the notion of normal terms to a notion of normal proofs, expressing that the hypotheses of the axioms never need to be all detached (since otherwise a simplification can happen).

Conversely, the non provability in intuitionistic logic ofPeirce's law can be transferred back to combinatory logic: there is no typed term of combinatory logic that is typable with type

((α →β) →α) →α.

Results on the completeness of some sets of combinators or axioms can also be transferred. For instance, the fact that the combinatorX constitutes aone-point basis of (extensional) combinatory logic implies that the single axiom scheme

(((α → (β →γ)) → ((α →β) → (α →γ))) → ((δ → (ε →δ)) →ζ)) →ζ,

which is theprincipal type ofX, is an adequate replacement to the combination of the axiom schemes

α → (β →α) and

(α → (β →γ)) → ((α →β) → (α →γ)).

AfterCurry emphasized the syntactic correspondence between intuitionisticHilbert-style deduction and typedcombinatory logic,Howard made explicit in 1969 a syntactic analogy between the programs ofsimply typed lambda calculus and the proofs ofnatural deduction. Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus ofsequents (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly) with implicit weakening and the right-hand side shows the typing rules oflambda calculus. In the left-hand side, Γ, Γ₁ and Γ₂ denote ordered sequences of formulas while in the right-hand side, they denote sequences of named (i.e., typed) formulas with all names different.

Intuitionistic implicational natural deduction	Lambda calculus type assignment rules
${\displaystyle \frac{}{{\mathrm{\Gamma }}_1,\alpha ,{\mathrm{\Gamma }}_2⊢\alpha }\text{Ax}}$	${\displaystyle \frac{}{{\mathrm{\Gamma }}_1,x:\alpha ,{\mathrm{\Gamma }}_2⊢x:\alpha }}$
${\displaystyle \frac{\mathrm{\Gamma },\alpha ⊢\beta }{\mathrm{\Gamma }⊢\alpha \to \beta }\to I}$	${\displaystyle \frac{\mathrm{\Gamma },x:\alpha ⊢t:\beta }{\mathrm{\Gamma }⊢(\lambda x:\alpha .t):\alpha \to \beta }}$
${\displaystyle \frac{\mathrm{\Gamma }⊢\alpha \to \beta \mathrm{\Gamma }⊢\alpha }{\mathrm{\Gamma }⊢\beta }\to E}$	${\displaystyle \frac{\mathrm{\Gamma }⊢t:\alpha \to \beta \mathrm{\Gamma }⊢u:\alpha }{\mathrm{\Gamma }⊢tu:\beta }}$

To paraphrase the correspondence, proving Γ ⊢α means having a program that, given values with the types listed in Γ, manufactures an object of typeα. An axiom/hypothesis corresponds to the introduction of a new variable with a new, unconstrained type, the→ I rule corresponds to function abstraction and the→ E rule corresponds tofunction application. Observe that the correspondence is not exact if the context Γ is taken to be a set of formulas as, e.g., the λ-terms λx.λy.x and λx.λy.y of typeα →α →α would not be distinguished in the correspondence. Examples are givenbelow.

Howard showed that the correspondence extends to other connectives of the logic and other constructions of simply typed lambda calculus. Seen at an abstract level, the correspondence can then be summarized as shown in the following table. Especially, it also shows that the notion of normal forms inlambda calculus matchesPrawitz's notion of normal deduction innatural deduction, from which it follows that the algorithms for thetype inhabitation problem can be turned into algorithms for decidingintuitionistic provability.

Howard's correspondence naturally extends to other extensions ofnatural deduction andsimply typed lambda calculus. Here is a non-exhaustive list:

• Girard-ReynoldsSystem F as a common language for both second-order propositional logic and polymorphic lambda calculus,
• higher-order logic and Girard'sSystem F_ω
• inductive types asalgebraic data type
• necessity${\displaystyle ◻}$ inmodal logic and staged computation^[11]
• possibility${\displaystyle ◊}$ inmodal logic and monadic types for effects^[10]
• Theλ_I calculus (where abstraction is restricted toλx.E wherex has at least one free occurrence inE) andCL_I calculus correspond torelevant logic.^[12]
• The local truth (∇) modality inGrothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".^[13]

At the time of Curry, and also at the time of Howard, the proofs-as-programs correspondence concerned onlyintuitionistic logic, i.e. a logic in which, in particular,Peirce's law wasnot deducible. The extension of the correspondence to Peirce's law and hence toclassical logic became clear from the work of Griffin on typing operators that capture the evaluation context of a given program execution so that this evaluation context can be later on reinstalled. The basic Curry–Howard-style correspondence for classical logic is given below. Note the correspondence between thedouble-negation translation used to map classical proofs to intuitionistic logic and thecontinuation-passing-style translation used to map lambda terms involving control to pure lambda terms. More particularly, call-by-name continuation-passing-style translations relates toKolmogorov's double negation translation and call-by-value continuation-passing-style translations relates to a kind of double-negation translation due to Kuroda.

A finer Curry–Howard correspondence exists for classical logic if one defines classical logic not by adding an axiom such asPeirce's law, but by allowing several conclusions in sequents. In the case of classical natural deduction, there exists a proofs-as-programs correspondence with the typed programs of Parigot'sλμ-calculus.

A proofs-as-programs correspondence can be settled for the formalism known asGentzen'ssequent calculus but it is not a correspondence with a well-defined pre-existing model of computation as it was for Hilbert-style and natural deductions.

Sequent calculus is characterized by the presence of left introduction rules, right introduction rule and a cut rule that can be eliminated. The structure of sequent calculus relates to a calculus whose structure is close to the one of someabstract machines. The informal correspondence is as follows:

N. G. de Bruijn used the lambda notation for representing proofs of the theorem checkerAutomath, and represented propositions as "categories" of their proofs. It was in the late 1960s at the same period of time Howard wrote his manuscript; de Bruijn was likely unaware of Howard's work, and stated the correspondence independently.^[14] Some researchers tend to use the term Curry–Howard–de Bruijn correspondence in place of Curry–Howard correspondence.

TheBHK interpretation interprets intuitionistic proofs as functions but it does not specify the class of functions relevant for the interpretation. If one takes lambda calculus for this class of function, then theBHK interpretation tells the same as Howard's correspondence between natural deduction and lambda calculus.

Kleene's recursiverealizability splits proofs of intuitionistic arithmetic into the pair of a recursive function and ofa proof of a formula expressing that the recursive function "realizes", i.e. correctly instantiates the disjunctions and existential quantifiers of the initial formula so that the formula gets true.

Kreisel's modified realizability applies to intuitionistic higher-order predicate logic and shows that thesimply typed lambda term inductively extracted from the proof realizes the initial formula. In the case of propositional logic, it coincides with Howard's statement: the extracted lambda term is the proof itself (seen as an untyped lambda term) and the realizability statement is a paraphrase of the fact that the extracted lambda term has the type that the formula means (seen as a type).

Gödel'sdialectica interpretation realizes (an extension of) intuitionistic arithmetic with computable functions. The connection with lambda calculus is unclear, even in the case of natural deduction.

Joachim Lambek showed in the early 1970s that the proofs of intuitionistic propositional logic and the combinators of typedcombinatory logic share a common equational theory, the theory ofcartesian closed categories. The expression Curry–Howard–Lambek correspondence is now used by some people^{[by whom?]} to refer to the relationships between intuitionistic logic, typed lambda calculus and cartesian closed categories. Under this correspondence, objects of a cartesian-closed category can be interpreted as propositions (types), and morphisms as deductions mapping a set of assumptions (typing context) to a valid consequent (well-typed term).^[15]

Lambek's correspondence is a correspondence of equational theories, abstracting away from dynamics of computation such as beta reduction and term normalization, and is not the expression of a syntactic identity of structures as it is the case for each of Curry's and Howard's correspondences: i.e. the structure of a well-defined morphism in a cartesian-closed category is not comparable to the structure of a proof of the corresponding judgment in either Hilbert-style logic or natural deduction. For example, it is not possible to state or prove that a morphism is normalizing, establish a Church-Rosser type theorem, or speak of a "strongly normalizing" cartesian closed category. To clarify this distinction, the underlying syntactic structure of cartesian closed categories is rephrased below.

Objects (propositions/types) include

• ${\displaystyle \mathrm{\top }}$ as an object
• given${\displaystyle \alpha }$ and${\displaystyle \beta }$ as objects, then${\displaystyle \alpha \times \beta }$ and${\displaystyle \alpha \to \beta }$ as objects.

Morphisms (deductions/terms) include

• identities:${\displaystyle {\text{id}}_{\alpha }:\alpha \to \alpha }$
• composition: if${\displaystyle t:\alpha \to \beta }$ and${\displaystyle u:\beta \to \gamma }$ are morphisms${\displaystyle u\circ t:\alpha \to \gamma }$ is a morphism
• terminal morphisms:${\displaystyle {\star }_{\alpha }:\alpha \to \mathrm{\top }}$
• products: if${\displaystyle t:\alpha \to \beta }$ and${\displaystyle u:\alpha \to \gamma }$ are morphisms,${\displaystyle (t,u):\alpha \to \beta \times \gamma }$ is a morphism
• projections:${\displaystyle {\pi }_{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha }$ and${\displaystyle {\pi }_{\alpha ,\beta ,2}:\alpha \times \beta \to \beta }$
• evaluation:${\displaystyle {\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta }$
• currying: if${\displaystyle t:\alpha \times \beta \to \gamma }$ is a morphism,${\displaystyle \lambda t:\alpha \to \beta \to \gamma }$ is a morphism.

Equivalently to the annotations above, well-defined morphisms (typed terms) in any cartesian-closed category can be constructed according to the followingtyping rules. The usual categorical morphism notation${\displaystyle f:\alpha \to \beta }$ is replaced withtyping context notation${\displaystyle \alpha ⊢f:\beta }$.

Identity:

${\displaystyle \frac{}{\alpha ⊢\text{id}:\alpha }}$

Composition:

${\displaystyle \frac{\alpha ⊢t:\beta \beta ⊢u:\gamma }{\alpha ⊢u\circ t:\gamma }}$

Unit type (terminal object):

${\displaystyle \frac{}{\alpha ⊢\star :\mathrm{\top }}}$

Cartesian product:

${\displaystyle \frac{\alpha ⊢t:\beta \alpha ⊢u:\gamma }{\alpha ⊢(t,u):\beta \times \gamma }}$

Left and right projection:

${\displaystyle \frac{}{\alpha \times \beta ⊢{\pi }_1:\alpha }\frac{}{\alpha \times \beta ⊢{\pi }_2:\beta }}$

Currying:

${\displaystyle \frac{\alpha \times \beta ⊢t:\gamma }{\alpha ⊢\lambda t:\beta \to \gamma }}$

Application:

${\displaystyle \frac{}{(\alpha \to \beta )\times \alpha ⊢\text{eval}:\beta }}$

Finally, the equations of the category are

• ${\displaystyle \text{id}\circ t=t}$
• ${\displaystyle t\circ \text{id}=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star =\text{id}}$ (if well-typed)
• ${\displaystyle \star \circ u=\star }$
• ${\displaystyle {\pi }_1\circ (t,u)=t}$
• ${\displaystyle {\pi }_2\circ (t,u)=u}$
• ${\displaystyle ({\pi }_1,{\pi }_2)=id}$
• ${\displaystyle (t_1,t_2)\circ u=(t_1\circ u,t_2\circ u)}$
• ${\displaystyle \text{eval}\circ (\lambda t\circ {\pi }_1,{\pi }_2)=t}$
• ${\displaystyle \lambda \text{eval}=\text{id}}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ {\pi }_1,{\pi }_2))}$

These equations imply the following${\displaystyle \eta }$-laws:

• ${\displaystyle ({\pi }_1\circ t,{\pi }_2\circ t)=t}$
• ${\displaystyle \lambda (\text{eval}\circ (t\circ {\pi }_1,{\pi }_2))=t}$

Now, there existst such that${\displaystyle {\alpha }_1\times \dots \times {\alpha }_n⊢t:\beta }$ iff${\displaystyle {\alpha }_1,\dots ,{\alpha }_n⊢\beta }$ is provable in implicational intuitionistic logic.

Thanks to the Curry–Howard correspondence, a typed expression whose type corresponds to a logical formula is analogous to a proof of that formula. Here are examples.

As an example, consider a proof of the theoremα →α. Inlambda calculus, this is the type of the identity functionI =λx.x and in combinatory logic, the identity function is obtained by applyingS =λfgx.fx(gx) twice toK =λxy.x. That is,I = ((SK)K). As a description of a proof, this says that the following steps can be used to proveα →α:

• instantiate the second axiom scheme with the formulasα,β →α andα to obtain a proof of(α → ((β →α) →α)) → ((α → (β →α)) → (α →α)),
• instantiate the first axiom scheme once withα andβ →α to obtain a proof ofα → ((β →α) →α),
• instantiate the first axiom scheme a second time withα andβ to obtain a proof ofα → (β →α),
• apply modus ponens twice to obtain a proof ofα →α

In general, the procedure is that whenever the program contains an application of the form (PQ), these steps should be followed:

1. First prove theorems corresponding to the types ofP andQ.
2. SinceP is being applied toQ, the type ofP must have the formα →β and the type ofQ must have the formα for someα andβ. Therefore, it is possible to detach the conclusion,β, via the modus ponens rule.

As a more complicated example, let's look at the theorem that corresponds to theB function. The type ofB is(β →α) → (γ →β) →γ →α.B is equivalent to (S (KS)K). This is our roadmap for the proof of the theorem(β →α) → (γ →β) →γ →α.

The first step is to construct (KS). To make the antecedent of theK axiom look like theS axiom, setα equal to(α →β →γ) → (α →β) →α →γ, andβ equal toδ (to avoid variable collisions):

K :α →β →α

K[α = (α →β →γ) → (α →β) →α →γ,β = δ] : ((α →β →γ) → (α →β) →α →γ) →δ → (α →β →γ) → (α →β) →α →γ

Since the antecedent here is justS, the consequent can be detached using Modus Ponens:

K S :δ → (α →β →γ) → (α →β) →α →γ

This is the theorem that corresponds to the type of (KS). Now applyS to this expression. TakingS as follows

S : (α →β →γ) → (α →β) →α →γ,

putα =δ,β =α →β →γ, andγ = (α →β) →α →γ, yielding

S[α =δ,β =α →β →γ,γ = (α →β) →α →γ] : (δ → (α →β →γ) → (α →β) →α →γ) → (δ → (α →β →γ)) → δ → (α →β) →α →γ

and then detach the consequent:

S (K S) : (δ →α →β →γ) → δ → (α →β) →α →γ

This is the formula for the type of (S (KS)). A special case of this theorem hasδ = (β →γ):

S (K S)[δ =β →γ] : ((β →γ) →α →β →γ) → (β →γ) → (α →β) →α →γ

This last formula must be applied toK. SpecializeK again, this time by replacingα with(β →γ) andβ withα:

K :α →β →α

K[α =β →γ,β =α] : (β →γ) →α → (β →γ)

This is the same as the antecedent of the prior formula so, detaching the consequent:

S (K S) K : (β →γ) → (α →β) →α →γ

Switching the names of the variablesα andγ gives us

(β →α) → (γ →β) →γ →α

which was what remained to prove.

The diagram below gives proof of(β →α) → (γ →β) →γ →α in natural deduction and shows how it can be interpreted as the λ-expressionλa.λb.λg.(a (bg)) of type(β →α) → (γ →β) →γ →α.

                                     a:β → α, b:γ → β, g:γ ⊢ b : γ → β    a:β → α, b:γ → β, g:γ ⊢ g : γ———————————————————————————————————  ————————————————————————————————————————————————————————————————————a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β————————————————————————————————————————————————————————————————————————               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α               ————————————————————————————————————               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α               ————————————————————————————————————————                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) → γ → α                        ————————————————————————————————————                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) → (γ → β) → γ → α

Recently, the isomorphism has been proposed as a way to define search space partition ingenetic programming.^[16] The method indexes sets of genotypes (the program trees evolved by the GP system) by their Curry–Howard isomorphic proof (referred to as a species).

As noted byINRIA research director Bernard Lang,^[17] the Curry-Howard correspondence constitutes an argument against the patentability of software: since algorithms are mathematical proofs, patentability of the former would imply patentability of the latter. A theorem could be private property; a mathematician would have to pay for using it, and to trust the company that sells it but keeps its proof secret and rejects responsibility for any errors.

The correspondences listed here go much farther and deeper. For example, cartesian closed categories are generalized byclosed monoidal categories. Theinternal language of these categories is thelinear type system (corresponding tolinear logic), which generalizes simply-typed lambda calculus as the internal language of cartesian closed categories. Moreover, these can be shown to correspond tocobordisms,^[18] which play a vital role instring theory.

An extended set of equivalences is also explored inhomotopy type theory. Here,type theory is extended by theunivalence axiom ("equivalence is equivalent to equality") which permits homotopy type theory to be used as a foundation for all of mathematics (includingset theory and classical logic, providing new ways to discuss theaxiom of choice and many other things). That is, the Curry–Howard correspondence that proofs are elements of inhabited types is generalized to the notion ofhomotopic equivalence of proofs (as paths in space, theidentity type orequality type of type theory being interpreted as a path).^[19]

This article includes a list ofgeneral references, butit lacks sufficient correspondinginline citations. Please help toimprove this article byintroducing more precise citations.(April 2010) (Learn how and when to remove this message)

• Curry, H B (1934-09-20)."Functionality in Combinatory Logic".Proceedings of the National Academy of Sciences of the United States of America.20 (11):584–90.Bibcode:1934PNAS...20..584C.doi:10.1073/pnas.20.11.584.ISSN 0027-8424.PMC 1076489.PMID 16577644.
• Curry, Haskell B; Feys, Robert (1958). Craig, William (ed.).Combinatory Logic. Studies in Logic and the Foundations of Mathematics. Vol. 1. North-Holland Publishing Company.LCCN a59001593; with two sections by Craig, William; see paragraph 9E{{cite book}}: CS1 maint: postscript (link)
• De Bruijn, Nicolaas (1968),Automath, a language for mathematics, Department of Mathematics,Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in:Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.
• Howard, William A. (September 1980) [original paper manuscript from 1969],"The formulae-as-types notion of construction"(PDF), inSeldin, Jonathan P.;Hindley, J. Roger (eds.),To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,Academic Press, pp. 479–490,ISBN 978-0-12-349050-6.

• Moggi, Eugenio (1991),"Notions of Computation and Monads"(PDF),Information and Computation,93 (1):55–92,doi:10.1016/0890-5401(91)90052-4
• Davies, Rowan; Pfenning, Frank (2001),"A Modal Analysis of Staged Computation"(PDF),Journal of the ACM,48 (3):555–604,CiteSeerX 10.1.1.3.5442,doi:10.1145/382780.382785,S2CID 52148006
• Pfenning, Frank; Davies, Rowan (2001),"A Judgmental Reconstruction of Modal Logic"(PDF),Mathematical Structures in Computer Science,11 (4):511–540,CiteSeerX 10.1.1.43.1611,doi:10.1017/S0960129501003322,S2CID 16467268
• Benton; Bierman; de Paiva (1998), "Computational types from a logical perspective",Journal of Functional Programming,8 (2):177–193,CiteSeerX 10.1.1.258.6004,doi:10.1017/s0956796898002998,S2CID 6149614
• Griffin, Timothy G. (1990), "The Formulae-as-Types Notion of Control",Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17–19 Jan 1990, pp. 47–57,doi:10.1145/96709.96714,ISBN 978-0-89791-343-0,S2CID 3005134.
• Parigot, Michel (1992), "Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction",International Conference on Logic Programming and Automated Reasoning: LPAR '92 Proceedings, St. Petersburg, Russia, Lecture Notes in Computer Science, vol. 624,Springer-Verlag, pp. 190–201,ISBN 978-3-540-55727-2.
• Herbelin, Hugo (1995), "A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure", in Pacholski, Leszek; Tiuryn, Jerzy (eds.),Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25–30, 1994, Selected Papers, Lecture Notes in Computer Science, vol. 933,Springer-Verlag, pp. 61–75,ISBN 978-3-540-60017-6.
• Gabbay, Dov;de Queiroz, Ruy (1992). "Extending the Curry–Howard interpretation to linear, relevant and other resource logics".Journal of Symbolic Logic. Vol. 57. Association for Symbolic Logic. pp. 1319–1365.doi:10.2307/2275370.JSTOR 2275370.S2CID 7159005.. (Full version of the paper presented atLogic Colloquium '90, Helsinki. Abstract inJSL 56(3):1139–1140, 1991.)
• de Queiroz, Ruy; Gabbay, Dov (1994), "Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality", in Dekker, Paul; Stokhof, Martin (eds.),Proceedings of the Ninth Amsterdam Colloquium, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–565,ISBN 978-90-74795-07-4.
• de Queiroz, Ruy; Gabbay, Dov (1995),"The Functional Interpretation of the Existential Quantifier",Bulletin of the Interest Group in Pure and Applied Logics, vol. 3, pp. 243–290. (Full version of a paper presented atLogic Colloquium '91, Uppsala. Abstract inJSL 58(2):753–754, 1993.)
• de Queiroz, Ruy; Gabbay, Dov (1997), "The Functional Interpretation of Modal Necessity", in de Rijke, Maarten (ed.),Advances in Intensional Logic, Applied Logic Series, vol. 7,Springer-Verlag, pp. 61–91,ISBN 978-0-7923-4711-8.
• de Queiroz, Ruy; Gabbay, Dov (1999),"Labelled Natural Deduction", in Ohlbach, Hans-Juergen; Reyle, Uwe (eds.),Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, Trends in Logic, vol. 7, Kluwer, pp. 173–250,ISBN 978-0-7923-5687-5.
• de Oliveira, Anjolina; de Queiroz, Ruy (1999), "A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction",Logic Journal of the Interest Group in Pure and Applied Logics, vol. 7,Oxford University Press, pp. 173–215. (Full version of a paper presented at2nd WoLLIC'95, Recife. Abstract inJournal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005),Adapting Proofs-as-Programs: The Curry–Howard Protocol, Monographs in Computer Science,Springer,ISBN 978-0-387-23759-6, concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina (2011), "The Functional Interpretation of Direct Computations",Electronic Notes in Theoretical Computer Science,269,Elsevier:19–40,doi:10.1016/j.entcs.2011.03.003. (Full version of a paper presented atLSFA 2010, Natal, Brazil.)

• de Queiroz, Ruy J.G.B. (1994), "Normalisation and language-games",Dialectica,48 (2):83–123,doi:10.1111/j.1746-8361.1994.tb00107.x,JSTOR 42968904. (Early version presented atLogic Colloquium '88, Padova. Abstract inJSL 55:425, 1990.)
• de Queiroz, Ruy J.G.B. (2001),"Meaning, function, purpose, usefulness, consequences – interconnected concepts",Logic Journal of the Interest Group in Pure and Applied Logics, vol. 9, pp. 693–734. (Early version presented atFourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)
• de Queiroz, Ruy J.G.B. (2008), "On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics",Studia Logica,90 (2):211–247,doi:10.1007/s11225-008-9150-5,S2CID 11321602.

• De Bruijn, Nicolaas Govert (1995),"On the roles of types in mathematics"(PDF), in Groote, Philippe de (ed.),De Groote 1995, pp. 27–54, the contribution of de Bruijn by himself.
• Geuvers, Herman (1995), "The Calculus of Constructions and Higher Order Logic",De Groote 1995, pp. 139–191, contains a synthetic introduction to the Curry–Howard correspondence.
• Gallier, Jean H. (1995),"On the Correspondence between Proofs and Lambda-Terms"(PDF),De Groote 1995, pp. 55–138, archived fromthe original(PDF) on 2017-07-05, contains a synthetic introduction to the Curry–Howard correspondence.
• Goldblatt, Robert (2006)."Grothendieck Topology as Intuitionistic Modality"(PDF). In Gabbay, Dov M.; Woods, John (eds.).Handbook of the History of Logic, vol. 7:Logic and the Modalities in the Twentieth Century. Amsterdam: Elsevier. pp. 76–81.ISBN 978-0-444-51622-0.
• Wadler, Philip (2014),"Propositions as Types"(PDF),Communications of the ACM,58 (12):75–84,doi:10.1145/2699407,S2CID 11957500

• Coecke, Bob; Kissinger, Aleks (2017).Picturing Quantum Processes. Cambridge University Press.ISBN 978-1-107-10422-8.
• Kennedy, Juliette; Kossak, Roman, eds. (2011).Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies. Cambridge University Press.ISBN 978-1-107-00804-5.
• Baez, John C.; Stay, Mike (2011)."Physics, Topology, Logic and Computation: A Rosetta Stone"(PDF). In Coecke, Bob (ed.).New Structures for Physics. Lecture Notes in Physics. Vol. 813. Berlin: Springer. pp. 95–174.arXiv:0903.0340.
• Casadio, Claudia; Scott, Philip J. (2021).Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer.ISBN 978-3-030-66545-6.
• Lambek, Joachim; Scott, P. J. (1989).Introduction to higher order categorical logic. Cambridge New York Port Chester [etc.]: Cambridge university press.ISBN 0521356539.
• De Groote, Philippe, ed. (1995),The Curry–Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain), vol. 8, Academia-Bruylant,ISBN 978-2-87209-363-2, reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998],Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics, vol. 149,Elsevier Science,CiteSeerX 10.1.1.17.7385,ISBN 978-0-444-52077-7, notes on proof theory and type theory, that includes a presentation of the Curry–Howard correspondence, with a focus on the formulae-as-types correspondence
• Girard, Jean-Yves (1987–1990),Proof and Types, Cambridge Tracts in Theoretical Computer Science, vol. 7, Translated by and with appendices by Lafont, Yves and Taylor, Paul, Cambridge University Press,ISBN 0-521-37181-3, archived fromthe original on 2008-04-18, notes on proof theory with a presentation of the Curry–Howard correspondence.
• Thompson, Simon (1991),Type Theory and Functional Programming, Addison–Wesley,ISBN 0-201-41667-0.
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005),Adapting Proofs-as-Programs: The Curry–Howard Protocol, Monographs in Computer Science,Springer,ISBN 978-0-387-23759-6, concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
• Binard, F.; Felty, A. (2008),"Genetic programming with polymorphic types and higher-order functions"(PDF),Proceedings of the 10th annual conference on Genetic and evolutionary computation, Association for Computing Machinery, pp. 1187–94,doi:10.1145/1389095.1389330,ISBN 9781605581309,S2CID 3669630
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011),The Functional Interpretation of Logical Deduction, Advances in Logic, vol. 5, Imperial College Press/World Scientific,ISBN 978-981-4360-95-1.

• Johnstone, P.T. (2002), "D4.2 λ-Calculus and cartesian closed categories",Sketches of an Elephant, A Topos Theory Compendium, vol. 2, Clarendon Press, pp. 951–962,ISBN 978-0-19-851598-2 — gives acategorical view of "what happens" in the Curry–Howard correspondence.

The WikibookHaskell has a page on the topic of:The Curry–Howard isomorphism

• Howard on Curry-Howard
• The Curry–Howard Correspondence in Haskell
• The Monad Reader 6: Adventures in Classical-Land: Curry–Howard in Haskell, Pierce's law.

• 1934 in computing
• 1958 in computing
• 1969 in computing
• Dependently typed programming
• Proof theory
• Logic in computer science
• Type theory
• Philosophy of computer science

• Articles with short description
• Short description is different from Wikidata
• Articles with specifically marked weasel-worded phrases from October 2023
• Articles lacking in-text citations from April 2010
• All articles lacking in-text citations
• CS1 maint: postscript