Call-by-name reduction and cut-elimination in classical logic
From MaRDI portal
Publication:2482842
DOI10.1016/j.apal.2008.01.002zbMath1136.03036OpenAlexW2014371684MaRDI QIDQ2482842
Publication date: 24 April 2008
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2008.01.002
Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Classical propositional logic (03B05) Combinatory logic and lambda calculus (03B40)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Explicit substitution. On the edge of strong normalization
- Explicit Substitutions and Reducibility
- The duality of computation
- A Sequent Calculus for Type Theory
- A new deconstructive logic: linear logic
- Proofs of strong normalisation for second order classical natural deduction
- Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
- Call-by-value is dual to call-by-name
- Foundations of Software Science and Computation Structures
- Term Rewriting and Applications
This page was built for publication: Call-by-name reduction and cut-elimination in classical logic