A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
The Curry-Howard correspondence is a deep isomorphism between logic and computation: propositions correspond to types, proofs correspond to programs, and proof normalization corresponds to program evaluation. An implication A -> B is a function type; a proof of A -> B is a function that takes a proof of A and produces a proof of B. A conjunction A AND B is a product type (pair); a disjunction A OR B is a sum type (tagged union). Under this correspondence, type-checking IS proof-checking — a well-typed program is simultaneously a valid proof. This insight unifies logic, type theory, and programming language theory into a single framework.
The Curry-Howard correspondence, discovered independently by Haskell Curry (1930s-1950s) and William Howard (1969), reveals that two seemingly different intellectual traditions — mathematical logic and the theory of computation — are actually the same thing viewed from different perspectives. The correspondence is not a loose analogy but a precise, structural isomorphism: every concept in one domain has an exact counterpart in the other.
The basic dictionary is this: propositions are types, proofs are programs, and proof simplification is computation. The logical connective "A implies B" corresponds to the function type A -> B. A proof of "A implies B" is a function that takes a proof of A and returns a proof of B. The connective "A and B" corresponds to the product type (A, B) — a pair. A proof of a conjunction is a pair of proofs, one for each conjunct. "A or B" corresponds to the sum type A + B (a tagged union). A proof of a disjunction provides one of the two proofs, tagged with which disjunct it proves. "False" corresponds to the empty type (no inhabitants). "True" corresponds to the unit type (one trivial inhabitant).
This correspondence is constructive: it aligns with intuitionistic (constructive) logic, not classical logic. In constructive logic, proving "A or B" requires actually producing a proof of A or a proof of B — you cannot just argue by contradiction. Under Curry-Howard, this makes sense: constructing a value of type A + B requires producing either a Left(a) or a Right(b). The classical law of excluded middle (A or not A) would require a program that, for any type A, either produces a value of A or a function A -> Void — which is not computable in general. Classical reasoning can be added to the correspondence (it corresponds to control operators like call/cc), but the natural alignment is with constructive logic.
The correspondence extends to quantifiers via dependent types. The universal quantifier "for all x : A, B(x)" corresponds to a dependent function type (x : A) -> B(x): a function that takes an x of type A and produces a value of type B(x), where the output type depends on the input value. The existential quantifier "there exists x : A such that B(x)" corresponds to a dependent pair type (x : A, B(x)): a pair of a witness x and a proof that B(x) holds. This extension takes Curry-Howard from propositional logic to full predicate logic and is the foundation of dependent type theory and proof assistants like Coq, Lean, and Agda.
The practical import is profound. Proof assistants implement the correspondence directly: you prove theorems by writing programs in a dependently-typed language, and type-checking IS proof-checking. When Coq accepts a term of a given type, it has mechanically verified that the corresponding proposition is true. The correspondence also explains why termination matters: a non-terminating program of type A would "prove" A regardless of whether A is actually true, collapsing the logic into inconsistency. This is why proof assistants restrict to total (terminating) functions, ensuring that every type inhabitant is a genuine proof.