For personal study only. Below you find

- 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.