- some few pages of my transcription to LaTeX of the paper 'Howard, The formulae-as-types notion of construction'">
- An excerpt of Philip Wadler paper "Propositions as types".
From
Philip Wadler, Propositions as types
[...] It is often referred to as the Curry-Howard Isomorphism, referring
to a correspondence observed by Curry in 1934 and refined by Howard in 1969
[...]
Motivated by Curry's observation, Howard pointed out that there
is a similar correspondence between
natural deduction, on the one hand, and
simply-typed lambda calculus, on the other,
and he made explicit the third and deepest level:
[the simplification of proofs
corresponds to evaluation of programs].
Howard showed the correspondence extends to the other logical connectives,
conjunction and disjunction, by extending his lambda calculus with
constructs that represent pairs and disjoint sums.
Just as proof rules come in introduction and elimination pairs, so do
typing rules: introduction rules correspond
to ways to define or construct a value of the given type, and
elimination rules correspond to ways to use or deconstruct values
of the given type.