Type Theory and Curry-Howard Correspondence

⚡ Key Takeaways

Type theory is a formal system in which every term carries a type, and the Curry–Howard correspondence establishes a precise dictionary equating propositions with types, proofs with programs, and proof normalization with program evaluation. Key result: intuitionistic logic and the simply typed λ-calculus are two faces of the same structure; this extends to dependent types ↔ predicate logic, and to cartesian closed categories. Applies to proof assistants (Coq, Lean, Agda), functional programming, and the foundations of constructive mathematics. Originating with Curry (1934), Howard (1969), and de Bruijn, Martin-Löf, and Lawvere.

💡 The Core Insight

A proposition is the type of its proofs. To prove $A \Rightarrow B$ is to give a method transforming any proof of $A$ into a proof of $B$ — i.e., a function of type $A \to B$ . Logical connectives become type constructors ( $\wedge \leftrightarrow \times$ , $\vee \leftrightarrow +$ , $\Rightarrow \leftrightarrow \to$ , $\forall \leftrightarrow \Pi$ , $\exists \leftrightarrow \Sigma$ ), inference rules become typing rules, and the act of running a proof corresponds to simplifying a redundant proof step. Logic, computation, and structure are unified.

DefinitionSimply Typed λ-Calculus (λ→)

Types are generated from a set of base types $o, \iota, \dots$ by the function arrow:

1

\quad \tau ::= o \mid \tau \to \tau

Derivation hint: read $\to$ as right-associative; $A \to B \to C$ means $A \to (B \to C)$ . Terms are variables, applications, and abstractions:

2

\quad M ::= x \mid (M\,M) \mid (\lambda x{:}\tau.\,M)

Derivation hint: $\lambda x{:}\tau.M$ binds $x$ in $M$ ; application associates left. A context $\Gamma$ is a finite list $x_1{:}A_1, \dots, x_n{:}A_n$ of variable–type pairs with distinct variables. The typing judgment $\Gamma \vdash M : A$ is derived by:

3

\quad \dfrac{(x{:}A)\in\Gamma}{\Gamma \vdash x : A}\ (\mathrm{var}) \qquad \dfrac{\Gamma, x{:}A \vdash M : B}{\Gamma \vdash \lambda x{:}A.\,M : A \to B}\ (\mathord{\to}\mathrm{I}) \qquad \dfrac{\Gamma \vdash M : A\to B \quad \Gamma \vdash N : A}{\Gamma \vdash (M\,N) : B}\ (\mathord{\to}\mathrm{E})

Derivation hint: abstraction discharges a hypothesis ( $\to$ introduction); application uses a function on an argument ( $\to$ elimination).

DefinitionCurry–Howard Dictionary

The correspondence is the table of identifications between logic and type theory:

4

\quad \begin{array}{lll} \textbf{Logic} & \textbf{Type theory} & \textbf{Constructor}\\ \text{proposition } A & \text{type } A & \\ \text{proof of } A & \text{term } M:A & \\ A \Rightarrow B & A \to B & \text{function}\\ A \wedge B & A \times B & \text{product / pair}\\ A \vee B & A + B & \text{coproduct / sum}\\ \top & \mathbf{1} & \text{unit}\\ \bot & \mathbf{0} & \text{empty}\\ \forall x{:}D.\,P(x) & \Pi_{x:D}\,P(x) & \text{dependent product}\\ \exists x{:}D.\,P(x) & \Sigma_{x:D}\,P(x) & \text{dependent sum} \end{array}

Derivation hint: each connective's introduction/elimination rules match the constructor/destructor typing rules exactly.

TheoremCurry–Howard Isomorphism

There is a bijection between 1. derivations of $A_1, \dots, A_n \vdash B$ in the natural-deduction system for intuitionistic propositional logic ( $\mathrm{IPL}$ ), and 2. (β-normal, up to renaming) terms $M$ with $x_1{:}A_1,\dots,x_n{:}A_n \vdash M : B$ in λ→ (with products and sums), such that proof normalization (detour/cut elimination) corresponds to β-reduction. Formally, if a proof $\pi$ reduces to $\pi'$ by removing an introduction-then-elimination detour, the associated terms satisfy $M_\pi \twoheadrightarrow_\beta M_{\pi'}$ .

TheoremCurry–Howard–Lambek (Categorical Form)

The following three are equivalent structures:

the term model of λ→ with products,
the proof theory of $\{\wedge, \Rightarrow, \top\}$ -IPL,
a cartesian closed category (CCC),

with $\times$ the product, $\top$ the terminal object $\mathbf 1$ , and $\to$ the exponential, satisfying the adjunction:

5

\quad \mathrm{Hom}(C \times A,\ B)\ \cong\ \mathrm{Hom}(C,\ B^A)

Derivation hint: this is currying — read left-to-right as $\lambda$ -abstraction over $A$ , right-to-left as application; the natural iso is the defining universal property of the exponential.

ProofProofs-as-terms by induction on derivations

We define a translation $(-)^\ast$ from IPL natural-deduction derivations to λ-terms and show it preserves and reflects structure.

Step 1 — Hypotheses. A use of hypothesis $A_i$ at the leaf becomes a variable $x_i : A_i$ . This matches the $(\mathrm{var})$ rule [3].

Step 2 — Implication introduction. A derivation of $B$ from an extra hypothesis $A$ , discharged to conclude $A \Rightarrow B$ , becomes

6

\quad \dfrac{\;[x{:}A]\;\;\vdots\;\; M:B\;}{\lambda x{:}A.\,M : A\to B}

Derivation hint: discharging the assumption $A$ is exactly binding the variable $x$ ; the bracketed $[x{:}A]$ is the discharged hypothesis.

Step 3 — Implication elimination. Modus ponens (from $A\Rightarrow B$ and $A$ infer $B$ ) becomes application $(M\,N):B$ , matching $(\mathord{\to}\mathrm{E})$ .

Step 4 — Detours = redexes. A detour is an introduction immediately followed by the matching elimination, e.g. $\to$ I then $\to$ E:

7

\quad \dfrac{\dfrac{[x{:}A]\;\vdots\;M:B}{\lambda x.M : A\to B}\quad N:A}{(\lambda x.M)\,N : B}\ \rightsquigarrow\ M[N/x] : B

Derivation hint: removing the detour substitutes the proof $N$ of $A$ for the hypothesis $x$ — this is exactly β-reduction $(\lambda x.M)N \to_\beta M[x:=N]$ .

Step 5 — Conjunction. Pairing introduces $A\wedge B$ , projections eliminate it, with reductions $\pi_1\langle M,N\rangle \to M$ , $\pi_2\langle M,N\rangle \to N$ matching detour elimination for $\wedge$ .

Step 6 — Bijectivity. The inverse translation reads off a derivation from a typing derivation rule-by-rule. Since both are defined by structural recursion on the same set of rules, $(-)^\ast$ and its inverse are mutually inverse, giving the bijection. Preservation of normalization (Step 4) yields the dynamical part of the theorem. $\blacksquare$

∎

⚠️ Classical logic needs more

The plain isomorphism is with intuitionistic logic. The law of excluded middle $A \vee \neg A$ , double-negation elimination $\neg\neg A \Rightarrow A$ , and Peirce's law $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ are not inhabited in λ→. Classical logic corresponds to λ-calculi with control operators (Griffin 1990): `call/cc` has the type of Peirce's law. This is the Curry–Howard for classical logic (Parigot's λμ-calculus).

mathematician · Haskell B. Curry & William A. Howard | 1900–1982 / b. 1926

Curry, a combinatory-logic pioneer, observed in 1934 that the types of his combinators $K$ and $S$ mirror the axioms of implicational logic ( $A\Rightarrow B\Rightarrow A$ and $(A\Rightarrow B\Rightarrow C)\Rightarrow(A\Rightarrow B)\Rightarrow A\Rightarrow C$ ). Howard, in a 1969 manuscript circulated informally and published in 1980, extended the analogy to full natural deduction and crucially identified proof reduction with term reduction, turning a static analogy into a dynamic isomorphism. Per Martin-Löf later built an entire constructive foundation (intuitionistic type theory) on this principle.

🧠 Intuition

Think of a proposition not as something that is merely true or false, but as a collection of evidence. The proposition " $A \Rightarrow B$ " is not a truth value — it is the set of machines that convert any piece of $A$ -evidence into a piece of $B$ -evidence. To "prove" the implication is to build such a machine. Proving $A \wedge B$ means handing over both pieces of evidence (a pair). Proving $A \vee B$ means handing over one piece plus a tag saying which side it is (a tagged union) — this is why constructive disjunction is stronger than classical: you must know which disjunct holds. The empty type $\mathbf 0$ has no evidence, so a function $A \to \mathbf 0$ (a proof of $\neg A$ ) is a machine that, fed $A$ -evidence, manufactures the impossible — hence $A$ must itself be uninhabited.

Figure

The triple correspondence: logic, computation, and category theory as one structure

```svg

```

ExampleConstructing a proof term for

A \Rightarrow (B \Rightarrow A)

Given: the K-combinator proposition (weakening axiom).

Step 1. We need a term of type $A \to (B \to A)$ in the empty context.

Step 2. Introduce $x : A$ (intro of outer $\to$ ), goal becomes $B \to A$ .

Step 3. Introduce $y : B$ (intro of inner $\to$ ), goal becomes $A$ .

Step 4. Context is $x{:}A,\ y{:}B$ . Use $(\mathrm{var})$ : $x : A$ . Done.

Step 5. Re-abstract:

8

\quad \vdash\ \lambda x{:}A.\,\lambda y{:}B.\,x\ :\ A \to (B \to A)

Derivation hint: this is precisely Curry's combinator $K$ ; logically it is "if $A$ then ( $B$ implies $A$ )".

Boxed answer: $\boxed{K = \lambda x.\lambda y.\, x \ :\ A \to B \to A}$ — a valid intuitionistic proof, inhabited.

ExampleNormalizing a proof = running a program

Given: the term $M = (\lambda f{:}A\to A.\ \lambda x{:}A.\ f\,(f\,x))\ (\lambda y{:}A.\,y)$ , which proves $A \to A$ (apply "do twice" to the identity proof).

Step 1. Outer redex: substitute $f := \lambda y.y$ into $\lambda x.\, f(f\,x)$ :

9

\quad M \ \to_\beta\ \lambda x{:}A.\ (\lambda y.y)\big((\lambda y.y)\,x\big)

Derivation hint: β-reduce the outer application, replacing every $f$ .

Step 2. Inner redex $(\lambda y.y)\,x \to_\beta x$ :

10

\quad \lambda x.\ (\lambda y.y)\,x \ \to_\beta\ \lambda x{:}A.\,x

Derivation hint: identity applied to $x$ is $x$ ; one more β-step on the remaining redex.

Boxed answer: $\boxed{M \twoheadrightarrow_\beta \lambda x{:}A.\,x}$ . The "complicated" proof of $A\to A$ normalizes to the trivial identity proof — the cut-free / normal proof. Type is preserved at every step (Subject Reduction).

⚠️ Curry-style vs. Church-style typing

Do not conflate two presentations. In Church-style (explicit) typing, abstractions carry their domain annotation $\lambda x{:}A.M$ , every term has a unique type, and types are part of the syntax. In Curry-style (implicit) typing, terms are untyped λ-terms and a type assignment relation decides which types a term can have — a term may have many types (principal type via Hindley–Milner). The Curry–Howard correspondence is cleanest in the Church-style, propositions-as-types reading; Curry's original 1934 observation was, fittingly, the assignment view.

CounterexampleNot every classical tautology is a type

Peirce's law $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ is a classical tautology but is not inhabited in λ→. There is no closed term

11

\quad \vdash\ ?\ :\ ((A\to B)\to A)\to A

Derivation hint: try to build it — after introducing $k:(A\to B)\to A$ you must produce an $A$ ; the only way is to feed $k$ a function $A\to B$ , but you have no $A$ to feed that function, so you are stuck. The deadlock is exactly the absence of a control operator. This shows the correspondence is with intuitionistic, not classical, logic — a feature, not a bug: it forces proofs to be constructive (computational).

connection

Type theory sits at the crossroads of several fields. To Lambda Calculus it adds typing discipline guaranteeing strong normalization (every typed term halts). To Category Theory it connects via Cartesian Closed Categories, where the internal language of a CCC is λ→. To Intuitionistic Logic it provides the proofs-as-programs semantics, and to Proof Theory it identifies normalization with Gentzen's cut elimination. The dependent extension yields Martin-Löf Type Theory, whose modern reinterpretation — identity types as paths — is Homotopy Type Theory, linking to Algebraic Topology and Higher Category Theory. The polymorphic fragment System F connects to second-order logic and parametricity.

🔬 Where this appears

⏳ History

- 1902 — Russell discovers his paradox; ramified type theory introduced in Principia Mathematica (1910–13) to block self-reference, the first "type theory."

- 1934 — Curry notes the correspondence between combinator types and Hilbert-style axiom schemes for implicational logic.

- 1940 — Church introduces the simply typed λ-calculus, a consistent higher-order logic avoiding the inconsistency of his earlier untyped system.

- 1958 — Gödel's Dialectica interpretation (System T) gives primitive-recursive functionals of finite type, a computational reading of arithmetic.

- 1965 — Tait proves strong normalization for System T via reducibility candidates, the key proof-theoretic technique.

- 1969 — Howard's manuscript "The formulae-as-types notion of construction" makes proof reduction = β-reduction explicit (published 1980).

- 1970–72 — Girard invents System F (polymorphism) and Reynolds independently rediscovers it (1974); de Bruijn builds Automath, the first practical proof checker.

- 1972–84 — Per Martin-Löf develops intuitionistic (dependent) type theory with

\Pi

,

\Sigma

, and identity types — a complete constructive foundation.

- 1980s–90s — Lambek formalizes the CCC correspondence; Coquand–Huet's Calculus of Constructions (1988) underlies Coq; Griffin (1990) extends Curry–Howard to classical logic via `call/cc`.

- 2006–13 — Voevodsky's univalence axiom launches Homotopy Type Theory, reinterpreting types as ∞-groupoids and equality as homotopy.

open-problem

Several deep tensions remain active research. (1) Univalence and computation: the original HoTT univalence axiom breaks canonicity (some closed terms fail to compute to a value); cubical type theory (Cohen–Coquand–Huet–Mörtberg 2016) restores computational content, but a fully satisfactory, fully general computational interpretation of higher inductive types is still being refined. (2) Decidability frontiers: type checking is decidable for λ→ and Martin-Löf type theory with normalization, but adding extensional equality (reflection) makes it undecidable; locating the exact boundary of usable-yet-decidable systems is ongoing. (3) Classical realizability: giving constructive/computational meaning to genuinely classical and choice principles (Krivine's classical realizability) and reconciling them with intuitionistic foundations remains partly open. (4) Coherence: managing the infinite tower of coherence conditions for higher categories internally in type theory — the problem of semi-simplicial types and a fully synthetic $(\infty,1)$ -category theory — is a major unsolved challenge.

Type Theory and Curry-Howard Correspondence

Formal Statement

Why It Holds / Derivation

Building Intuition

Worked Examples

Common Misconceptions

Connections

Real-World Applications

Historical Development

Subtleties & Limits

See Also