  At about the same time as strong normalization was studied, the Curry-Howard correspondence emerged. Curry had observed in his work on combinatory logic in the late 1950s the analogy between implication elimination in natural deduction and functional application (Curry and Feys 1958). The idea was as old as intuitionistic logic: by the “BHK-explanation” of the connectives and quantifiers (for Brouwer-Heyting-Kolmogorov), the forms of propositions in intuitionistic logic express prescriptions on how to prove those propositions: a conjunction A &amp; B is proved by proving A and B separately, a disjunction A ∨ B by proving one of A and B, and an implication A ⊃ B by showing how to convert any proof of A into some proof of B, and so on. These explanations come very close to the introduction rules of natural deduction, but it remains unknown what their effect on Gentzen's thought was.