 Implicational Curry-Howard correspondence

In the implicational fragments, assumptions correspond to typed variables, implication introduction to lambda abstraction, and implication elimination to function application. Typing derivations in the simply typed lambda calculus correspond inductively to natural-deduction proofs.