= Solution
Under the <Curry-Howard correspondence>, <Intuitionistic propositional logic> propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The <logical implication> $A\to B$ corresponds to the function type, <logical conjunction> $A\wedge B$ to the product type, <logical disjunction> $A\vee B$ to the sum type, <logical truth> to the unit type, and <logical falsity> to the empty type.
The rules of <natural deduction> become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by <beta reduction> in the <simply typed lambda calculus>.
Back to article page
