Article contents
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language
Published online by Cambridge University Press: 12 March 2014
Abstract
We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.
We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2011
References
REFERENCES
- 4
- Cited by