Curry–Howard correspondence

General formulation

In its more general formulation, the Curry–Howard correspondence is a correspondence between formal proof calculi and type systems for models of computation. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs 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 to dependent 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 as Hilbert-style deduction system and combinatory logic, and, secondly, between some particular formulations of systems known as natural deduction and lambda calculus.

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

Corresponding systems

Intuitionistic Hilbert-style deduction systems and typed combinatory logic

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 of combinatory logic surprisingly corresponded to the respective axiom schemes α → (β → α) and (α → (β → γ)) → ((α → β) → (α → γ)) used in Hilbert-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 given below.

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 δ is derivable 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 of modus ponens)

This can be formalized using inference 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 to intuitionistic logic means that some classical tautologies, such as Peirce's law ((α → β) → α) → α, are excluded from the correspondence.

Seen at a more abstract level, the correspondence can be restated as shown in the following table. Especially, the deduction theorem specific to Hilbert-style logic matches the process of abstraction 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 of reduction 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 of Peirce'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 combinator X constitutes a one-point basis of (extensional) combinatory logic implies that the single axiom scheme

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

which is the principal type of X, is an adequate replacement to the combination of the axiom schemes

α → (β → α) and

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

Intuitionistic natural deduction and typed lambda calculus

After Curry emphasized the syntactic correspondence between intuitionistic Hilbert-style deduction and typed combinatory logic, Howard made explicit in 1969 a syntactic analogy between the programs of simply typed lambda calculus and the proofs of natural deduction. Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents (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 of lambda 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.

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 to function 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 given below.

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 in lambda calculus matches Prawitz's notion of normal deduction in natural deduction, from which it follows that the algorithms for the type inhabitation problem can be turned into algorithms for deciding intuitionistic provability.

Howard's correspondence naturally extends to other extensions of natural deduction and simply typed lambda calculus. Here is a non-exhaustive list:

• Girard–Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus,
• higher-order logic and Girard's System F_ω
• inductive types as algebraic data type
• necessity ${\displaystyle ◻}$ in modal logic and staged computation
• possibility ${\displaystyle ◊}$ in modal logic and monadic types for effects
• The λ_I calculus (where abstraction is restricted to λx.E where x has at least one free occurrence in E) and CL_I calculus correspond to relevant logic.
• The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".

Classical logic and control operators

At the time of Curry, and also at the time of Howard, the proofs-as-programs correspondence concerned only intuitionistic logic, i.e. a logic in which, in particular, Peirce's law was not deducible. The extension of the correspondence to Peirce's law and hence to classical 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 the double-negation translation used to map classical proofs to intuitionistic logic and the continuation-passing-style translation used to map lambda terms involving control to pure lambda terms. More particularly, call-by-name continuation-passing-style translations relates to Kolmogorov'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 as Peirce'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.

Sequent calculus

A proofs-as-programs correspondence can be settled for the formalism known as Gentzen's sequent 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 some abstract machines. The informal correspondence is as follows:

Related proofs-as-programs correspondences

Prawitz's 1968 homomorphism

In a paper published in 1970, but drawn from a talk given at the First Scandinavian Logic Symposium, held in Åbo/Turku in 1968, Dag Prawitz defined a homomorphism between natural deduction derivations for minimal and intuitionistic first-order logic and construction terms from a language very similar to typed lambda calculus (the correspondence stems from a proof of soundness of those logics over the language of constructions terms). Although Prawitz's homomorphism is less powerful than the Curry-Howard isomorphism, with a stronger type-language it becomes an isomorphism too, though still missing dependent types. Prawitz was presumably unaware of Howard's work, especially since the talk from which his 1970 paper is drawn was delivered one year before Howard's manuscript started circulating.

The role of de Bruijn

N. G. de Bruijn used the lambda notation for representing proofs of the theorem checker Automath, 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. Some researchers tend to use the term Curry–Howard–de Bruijn correspondence in place of Curry–Howard correspondence.

BHK interpretation

The BHK 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 the BHK interpretation tells the same as Howard's correspondence between natural deduction and lambda calculus.

Realizability

Kleene's recursive realizability splits proofs of intuitionistic arithmetic into the pair of a recursive function and of a 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 the simply 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's dialectica interpretation realizes (an extension of) intuitionistic arithmetic with computable functions. The connection with lambda calculus is unclear, even in the case of natural deduction.

Curry–Howard–Lambek correspondence

Joachim Lambek showed in the early 1970s that the proofs of intuitionistic propositional logic and the combinators of typed combinatory logic share a common equational theory, the theory of cartesian closed categories. The expression Curry–Howard–Lambek correspondence is now used by some people 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).

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 following typing rules. The usual categorical morphism notation ${\displaystyle f:\alpha \to \beta }$ is replaced with typing 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 exists t 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.

Examples

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.

The identity combinator seen as a proof of α → α in Hilbert-style logic

As an example, consider a proof of the theorem α → α. In lambda calculus, this is the type of the identity function I = λx.x and in combinatory logic, the identity function is obtained by applying S = λfgx.fx(gx) twice to K = λxy.x. That is, I = ((S K) 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 (P Q), these steps should be followed:

1. First prove theorems corresponding to the types of P and Q.
2. Since P is being applied to Q, the type of P must have the form α → β and the type of Q must have the form α for some α and β. Therefore, it is possible to detach the conclusion, β, via the modus ponens rule.

The composition combinator seen as a proof of (β → α) → (γ → β) → γ → α in Hilbert-style logic

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

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

K : α → β → α

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

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

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

This is the theorem that corresponds to the type of (K S). Now apply S to this expression. Taking S as follows

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

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

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

and then detach the consequent:

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

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

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

This last formula must be applied to K. Specialize K 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 normal proof of (β → α) → (γ → β) → γ → α in natural deduction seen as a λ-term

The diagram below gives proof of (β → α) → (γ → β) → γ → α in natural deduction and shows how it can be interpreted as the λ-expression λa.λb.λg.(a (b g)) 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) : (β → α) → (γ → β) → γ → α

Other applications

Recently, the isomorphism has been proposed as a way to define search space partition in genetic programming. 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 by INRIA research director Bernard Lang, 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.

Symbolic reasoning in LLMs via code execution as a second process

Cognitive scientists have used dual process theory, which contrasts fast, intuitive "System 1" thinking with slow, deliberate "System 2" thinking, as a framework for analyzing how large language models (LLMs) reason and make decisions. Separately, a common engineering technique lets a model write and run computer code while working on a problem: rather than predicting an answer directly in text, the model writes a short program, an external interpreter executes it, and the model reads back the result. Delegating calculation to an interpreter in this way has been shown to reduce arithmetic and logical errors.

The Curry–Howard correspondence clarifies what running code can and cannot establish. Under the correspondence, a proof is a well-typed program and the proposition it proves is that program's type, so checking a proof amounts to type-checking a program; the logical content lies in the type system rather than in execution. General-purpose languages such as Python, SQL, and JavaScript were not designed as proof systems, and researchers in formalized mathematics have argued that proofs and programs play fundamentally different epistemic roles, so the analogy between coding and proving is limited in practice. In addition, the modal operators □ (necessity) and ◇ (possibility) acquire computational interpretations only in specialized modal type systems, which mainstream programming languages lack.

Proof assistants such as Rocq, Lean, and Agda are built directly on the correspondence: a theorem is stated as a type, and a machine-checked proof is a program of that type. Combining LLMs with these systems (all of which can be run as code execution, along with provers such as Sympy) produces reasoning that is verified rather than merely executed. AlphaProof, a system developed by Google DeepMind, used reinforcement learning to train a model to write Lean proofs on a curriculum of tens of millions of automatically formalized problem statements; every proof it produces is checked by Lean, and the system achieved a score equivalent to a silver medal at the 2024 International Mathematical Olympiad. Machine-checked reasoning in higher-order modal logic is also achievable by embedding modal logic into the logic of an existing prover, an approach used to formally verify Gödel's ontological proof. A remaining obstacle is autoformalization: reliably translating mathematical statements from natural language into formal language.

Some researchers have proposed applying the correspondence directly to LLM reasoning. One 2025 proposal treats each step of a model's chain-of-thought as a typed logical inference, so that a reasoning trace which converts into a well-typed proof serves as a verifiable certificate of its own correctness. Reviews of the field caution, however, that proof generation has proven considerably more brittle for LLMs than code generation, and that the elegance of the correspondence does not by itself close this gap.

Generalizations

The correspondences listed here go much farther and deeper. For example, cartesian closed categories are generalized by closed monoidal categories. The internal language of these categories is the linear type system (corresponding to linear logic), which generalizes simply-typed lambda calculus as the internal language of cartesian closed categories. Moreover, these can be shown to correspond to cobordisms, which play a vital role in string theory.

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