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]
@article{Gabbay11-2, title = {A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language}, author = {Michael Gabbay}, year = {2011}, url = {http://projecteuclid.org/euclid.jsl/1305810770}, tags = {programming languages, logic programming, programming, logic}, researchr = {https://researchr.org/publication/Gabbay11-2}, cites = {0}, citedby = {0}, journal = {Journal of Symbolic Logic}, volume = {76}, number = {2}, pages = {673-699}, }