Curry–Howard Correspondence

The Curry–Howard correspondence is a structural relationship between logic and computation: propositions correspond to types, proofs to terms inhabiting those types, and proof simplification to program evaluation. Its standard example connects intuitionistic logic with typed lambda calculus. Rather than asserting that arbitrary software constitutes a proof, it identifies matching rules within specified logical and computational systems. It provides a foundation for connections among proof theory, type theory, and computer science. (homepages.inf.ed.ac.uk)

Historical development

In 1934, Haskell Curry observed that the types assigned to certain combinators could be read as provable formulas of implicational logic. William Howard developed the deeper relationship between natural deduction and typed lambda calculus in a manuscript circulated in 1969 and published in 1980 under the title The Formulae-as-Types Notion of Construction. Howard also identified the correspondence between simplifying proofs and evaluating programs. (homepages.inf.ed.ac.uk)

The correspondence is closely related to the Brouwer–Heyting–Kolmogorov interpretation, which explains logical connectives through constructions establishing them. Subsequent developments, including de Bruijn’s Automath and Martin-Löf’s type theory, extended propositions-as-types ideas into systems for expressing and checking mathematics. The name therefore denotes a family of related correspondences, rather than one theorem covering every logic and programming language. (homepages.inf.ed.ac.uk)

Propositions, types, and judgments

The basic distinction is between a proposition and evidence establishing it. A type represents the proposition; a term of that type represents a particular proof. The judgment

means computationally that term $t$ has type $A$ under the variable declarations in context $\Gamma$. Logically, it means that $t$ encodes a derivation of proposition $A$ from the assumptions represented by that context. Assumptions become typed variables, and inference rules become rules for forming typed terms. (arxiv.org)

A proposition is provable precisely when its corresponding type is inhabited, within the chosen systems. This is stronger than comparing truth values: distinct terms may record distinct proofs of the same proposition. Calling the relationship an isomorphism emphasizes preservation of structure, although the precise statement depends on the calculi and the equivalences imposed on proofs and terms. (arxiv.org)

Logical connectives as type constructors

For intuitionistic propositional logic, the main correspondences are:

The introduction and elimination rules determine how this evidence is constructed and used. Conjunction introduction forms a pair; conjunction elimination selects a component. Disjunction elimination becomes case analysis, with branches handling each possible tag. Negation $\neg A$ is represented by $A\to\bot$. (cs.cmu.edu)

Implication illustrates the correspondence especially clearly. Assuming $x:A$ and constructing $t:B$ yields the lambda abstraction $\lambda x.t:A\to B$. Applying $f:A\to B$ to $a:A$ yields $f\,a:B$, corresponding to modus ponens. Thus the identity term $\lambda x.x:A\to A$ encodes the proof that $A$ implies itself. (docs.lean-lang.org)

Proof simplification and computation

The correspondence also describes dynamics. Suppose an implication is proved by introducing an assumption and is immediately used by implication elimination. The resulting detour can be removed by substituting the supplied proof for the assumption. Computationally, this is beta reduction:

where substitution avoids capturing free variables. Similarly, projecting the first component of a newly constructed pair reduces directly to that component. (cs.cmu.edu)

In the simply typed lambda calculus, well-typed terms are strongly normalizing: every reduction sequence terminates. The corresponding proof normalization result eliminates unnecessary detours from proofs. Unrestricted recursion cannot simply be added while retaining this logical interpretation: a diverging term may receive a type without producing evidence for its proposition. Termination restrictions therefore matter when programs are treated as proofs. (cs.cmu.edu)

Quantifiers and richer systems

Dependent types, whose structure can depend on values, extend the interpretation to quantification. A dependent function of type $\prod_{x:D}P(x)$ supplies evidence for $P(x)$ for each $x$, corresponding to universal quantification. A dependent pair $(x,p)$, with $p:P(x)$, supplies a witness and evidence for existential quantification. (cs.cmu.edu)

The direct interpretation is constructive. Classical logic requires additional treatment: the law of excluded middle does not follow from the basic intuitionistic rules. Classical principles can instead be introduced through additional axioms or interpreted using suitable computational mechanisms. Consequently, their computational meaning differs from the elementary function-and-pair interpretation. (docs.lean-lang.org)

Proof assistants and verification

In type-theoretic proof assistants, establishing a theorem means constructing a term with the required proposition as its type. Automated tactics can generate such terms, while checking their types verifies the resulting formal proofs. This architecture underlies applications to formal verification. (lean-lang.org)

Concrete implementations refine the general correspondence. Lean, for example, distinguishes propositions in Prop from computational data types and treats proofs of a proposition as definitionally equal. Its existential proofs contain witnesses, but those witnesses cannot generally be extracted into executable data by eliminating the proof. These restrictions show why propositions-as-types does not imply that every proof is an executable witness-producing program. (docs.lean-lang.org)