The Curry–Howard Correspondence
email Scott Turner
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.
| logic | programming |
|---|---|
| aggregates | |
| deduction, proof, or argument | program, expression, or term |
| proposition or formula | type 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 hypothesis | free name |
| valid argument | typable term |
| sound argument, i.e. valid argument with correct premises | typable term whose free names refer to built-in values, e.g. a library function |
| sequent | named context |
| tree-like structure of a natural deduction proof | abstract syntax tree of program |
| conjunction of propositions | cartesian product of types |
| disjunction of propositions | disjoint union of types |
| negation of a proposition, ¬A, or A⇒⊥ | |
| deduction of proposition A as copy of an available hypothesis | variable (reference) of type A |
| deduction ending with &-introduction rule | pair expression |
| deduction ending with &-elimination rule | expression selecting first or second |
| deduction ending with ⇒-introduction rule | lambda expression |
| deduction ending with ⇒-elimination rule | application 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 provable | type 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 proof | normalization/execution/evaluation of a term |
| classical logic embedded into constructive logic | cps (continuation passing style) program transformation |
| systems | |
| constructive/intuitionistic logic | typed lambda calculus |
| second order constructive logic | quantification over types (System F) |
| linear logic | linear type systems |
| sound proof procedure, i.e. provable formulas are valid | type 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. |
References
- 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).
- Griffin extends the constructive correspondence to classical logic.
- Introduction to Lambda Calculus, Barendregt & Barendsen
- J-Y. Girard, Proofs and Types, translated and with appendices by P. Taylor, Y. Lafont, 3
- Benjamin Pierce, Types and Programming Languages, 9.4, 8.3
- Philip Wadler, Proofs are Programs