Topic summary
Curry-Howard
Extracted from the Wikipedia article Curry–Howard correspondence.
Prawitz's 1968 homomorphism
In a paper published in 1970, but drawn from a talk given at the First Scandinavian Logic Symposium, held in Åbo/Turku in 1968, Dag Prawitz defined a homomorphism between natural deduction derivations for minimal and intuitionistic first-order logic and construction terms from a language very similar to typed lambda calculus (the correspondence stems from a proof of soundness of those logics over the language of constructions terms). Although Prawitz's homomorphism is less powerful than the Curry-Howard isomorphism, with a stronger type-language it becomes an isomorphism too, though still missing dependent types. Prawitz was presumably unaware of Howard's work, especially since the talk from which his 1970 paper is drawn was delivered one year before Howard's manuscript started circulating.