A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

Michael Gabbay. A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language. Journal of Symbolic Logic, 76(2):673-699, 2011. [doi]

Abstract

Abstract is missing.