  The Curry-Howard correspondence, from a paper by William Howard of  1969, but published only in 1980, is based on the  “formulas-as-types” principle, or in another jargon, on  the “propositions-as-sets” principle. A proposition is  thought of as its set of proofs. Truth of a proposition corresponds  to the non-emptyness of the set. Proofs of  A ⊃ B are now functions from (proofs  of) A to (proofs of) B and  A ⊃ B itself the set of such  functions. Thus, if f :  A ⊃ B and  a : A,  then functional application gives  f(a) : B. The reverse, corresponding to the introduction of an  implication, is captured by the principle of functional abstraction  of Alonzo Church's λ-calculus.