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

DOI10.1016/J.APAL.2008.01.002MaRDI QIDQ2482842zbMATH OpenOpenAlexFDO

Authors 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

classical logicCurry-Howard correspondencecut-eliminationsequent calculusstrong normalization

Mathematics Subject Classification ID

Classical propositional logic (03B05) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• scientific article; zbMATH DE number 1342291
• On semantics of a term calculus for classical logic
• Term Rewriting and Applications
• scientific article; zbMATH DE number 1302630

Cites work

• A new deconstructive logic: linear logic
• A Sequent Calculus for Type Theory
• Call-by-value is dual to call-by-name
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• Explicit substitution. On the edge of strong normalization
• Explicit substitutions and reducibility
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• Linear logic
• Proofs of strong normalisation for second order classical natural deduction
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• Term Rewriting and Applications
• The duality of computation

Cited in

(4)

• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• On semantics of a term calculus for classical logic
• Confluence for classical logic through the distinction between values and computations
• Compositional Z: confluence proofs for permutative conversion

This page was built for publication: Call-by-name reduction and cut-elimination in classical logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2482842)