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

DOI10.2178/jsl/1305810770zbMath1223.03038OpenAlexW2022792384MaRDI QIDQ3011126

Michael Gabbay

Publication date: 28 June 2011

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1305810770

zbMATH Keywords

cut-eliminationlogic programminglambda-calculusterm-sequent

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-incompleteness and finite lambda reduction models
• Uniform proofs as a foundation for logic programming
• A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing
• What is Logic?
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The Logic of Bunched Implications

This page was built for publication: A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language