Call-by-name reduction and cut-elimination in classical logic

DOI10.1016/j.apal.2008.01.002zbMath1136.03036OpenAlexW2014371684MaRDI QIDQ2482842

Kentaro Kikuchi

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

zbMATH Keywords

sequent calculuscut-eliminationstrong normalizationclassical logicCurry-Howard correspondence

Mathematics Subject Classification ID

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)

Compositional Z: confluence proofs for permutative conversion

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