 ## The Curry–Howard Correspondence

The Curry-Howard correspondence is the correspondence between the structure of proofs in logic, and the structure of computer programs. The following table displays many of its details.

logicprogramming
aggregates
deduction, proof, or argumentprogram, expression, or term
proposition or formulatype
or specification, i.e. abstraction of what the program does
constructive proof of a formula α program of type α
constructs
proof (with a parcel of hypotheses)functional term
premise or hypothesisfree name
valid argumenttypable term
sound argument, i.e. valid argument with correct premisestypable term whose free names refer to built-in values, e.g. a library function
sequentnamed context
tree-like structure of a natural deduction proofabstract syntax tree of program
conjunction of propositionscartesian product of types
disjunction of propositionsdisjoint union of types
negation of a proposition, ¬A, or A⇒⊥
deduction of proposition A as copy of an available hypothesisvariable (reference) of type A
deduction ending with &-introduction rulepair expression
deduction ending with &-elimination ruleexpression selecting first or second
deduction ending with ⇒-introduction rulelambda expression
deduction ending with ⇒-elimination ruleapplication expression
Pierce's law ((α ⇒ β) ⇒ α) ⇒ α `call/cc`
interpretations
A formula is the set of its possible deductions.
intuitionistic meaning of a proposition
what is required in order to prove a proposition
intuitionistic meaning of a connective (e.g. &) or of a proof of a proposition based on a connective
i.e. a converter of proofs
function
proposition P is provabletype P is inhabited by some term
constructive proof of α⇒β A “constructive” program of type α→β takes inputs of type α to outputs of type β.
classical proof of α⇒β A “classical” program of type α→β given an input of classical type α may jump to another context. Otherwise it will return a classical value of type β to the current context. Context jumps may lurk in values.
transformations
normalization/simplifying a proofnormalization/execution/evaluation of a term
classical logic embedded into constructive logic cps (continuation passing style) program transformation
systems
constructive/intuitionistic logictyped lambda calculus
second order constructive logicquantification over types (System F)
linear logiclinear type systems
sound proof procedure, i.e. provable formulas are validtype system that is safe/sound, i.e. Evaluation of a well-typed term whose free names are resolved will either terminate or continue without error.

There's a very helpful discussion of Curry-Howard at lambda-the-ultimate.

## References

1. W. A. Howard, The formulae-as-types notion of construction, in J. R. Hindley and J. P. Seldin, To H. B. Curry: Essays on combinatory logic, Lambda Calculus and Formalism, Academic Press (1980).
2. Griffin extends the constructive correspondence to classical logic.
3. Introduction to Lambda Calculus, Barendregt & Barendsen
4. J-Y. Girard, Proofs and Types, translated and with appendices by P. Taylor, Y. Lafont, 3
5. Benjamin Pierce, Types and Programming Languages, 9.4, 8.3
6. Philip Wadler, Proofs are Programs

Support open standards! 