A proof-theoretic treatment of -reduction with cut-elimination: -calculus as a logic programming language
From MaRDI portal
(Redirected from A proof-theoretic treatment of -reduction with cut-elimination: -calculus as a logic programming language)
A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
Recommendations
Cites work
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A simple class of Kripke-style models in which logic and computation have equal standing
- scientific article; zbMATH DE number 5318491 (Why is no real title available?)
- scientific article; zbMATH DE number 4090846 (Why is no real title available?)
- scientific article; zbMATH DE number 3557754 (Why is no real title available?)
- Order-incompleteness and finite lambda reduction models
- The Logic of Bunched Implications
- Uniform proofs as a foundation for logic programming
- What is Logic?
Cited in
(8)- A note on the proof theory of the -calculus
- A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG
- A Proof-Theoretic Account of Programming and the Role of Reduction Rules
- scientific article; zbMATH DE number 2079018 (Why is no real title available?)
- scientific article; zbMATH DE number 1418450 (Why is no real title available?)
- Lambda terms for natural deduction, sequent calculus and cut elimination
- Term sequent logic
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
This page was built for publication: A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3011126)
