Curry-Howard Correspondence

logic type-theory

Definition

Curry-Howard Correspondence

The Curry-Howard correspondence is a direct observation that logical systems and computational models are formally equivalent. It establishes an isomorphism between logic and type theory, where propositions correspond to types and proofs correspond to programs.

The Isomorphism

The correspondence relates elements of intuitionistic logic to constructs in the typed lambda calculus:

Logic (Propositions)	Computation (Types)
Proposition $A$	Type $A$
Proof of $A$	Program (Term) of type $A$
Implication $A⟹B$	Function Type $A\to B$
Conjunction $A\wedge B$	Product Type $A\times B$
Disjunction $A\vee B$	Sum Type $A+B$
Falsehood $\perp$	Empty Type (Bottom)
Modus Ponens	Function Application
Assumption Discharge	Abstraction ($\lambda$-abstraction)

Implications

• Theorem Proving: Proving a theorem is equivalent to writing a program that satisfies a specific type. If the type is inhabited (i.e., there exists a program of that type), the proposition is true.
• Program Correctness: A program is “correct by construction” if it corresponds to a valid proof in a sound logic.
• Simplification: Logical proof reduction (cut elimination) corresponds to program execution (beta reduction).

Dependent Types

Extending the correspondence to first-order logic (with quantifiers $\forall ,\exists$) requires Dependent Types, where types can depend on values. This forms the basis of proof assistants like Coq, Agda, and Lean.