Proof Polynomials vs. lambda-terms
Sergei Nikolaevich Artemov · 1998
Abstract : The Logic of Proofs provides a basic framework for the formalization of reasoning about proofs. It incorporates proof terms into the propositional language, using labeled logical operators t: with the intended reading of t:F being T is a proof of F. In the current paper we demonstrate how the typed lambda calculus and the modal lambda-calculus can be realized in the Logic of Proofs.