On semantics of a term calculus for classical logic

DOI10.2298/PIM1206079LMaRDI QIDQ2929866zbMATH OpenOpenAlexFDO

Authors Silvia Likavec, Pierre Lescanne

Publication date 14 November 2014

Published in Publications de l'Institut Math?matique (Belgrade), Publications de l'Institut Mathématique. Nouvelle Série (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2298/pim1206079l

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

confluencecontinuation semanticslambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Review text

Two subcalculi of the calculus introduced by Curien and Herbelin to provide the Curry-Howard correspondence for classical logic are investigated. One of these subcalculi corresponds to the ``call by value and the other to the ``call by name paradigm. A proof of confluence is given and soundness theorems are proven for both variants. A thorough overview of the work on continuation semantics is given.

Recommendations

• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• The stack calculus
• Constructive classical logic as CPS-calculus
• scientific article; zbMATH DE number 1231511
• Call-by-name reduction and cut-elimination in classical logic

Cited in

(17)

• A proof-theoretic foundation of abortive continuations
• Call-by-name reduction and cut-elimination in classical logic
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• A semantics of realisability for the classical propositional natural deduction
• On the computational representation of classical logical connectives
• Classical call-by-need sequent calculi: the unity of semantic artifacts
• Proofs, tests and continuation passing style
• Computation with classical sequents
• scientific article; zbMATH DE number 1222431 (Why is no real title available?)
• scientific article; zbMATH DE number 1231511 (Why is no real title available?)
• Classical logic, continuation semantics and abstract machines
• scientific article; zbMATH DE number 1948182 (Why is no real title available?)
• The untyped stack calculus and Böhm's theorem
• The stack calculus
• Confluence for classical logic through the distinction between values and computations
• Constructive classical logic as CPS-calculus
• Curry-Howard for sequent calculus at last!

This page was built for publication: On semantics of a term calculus for classical logic

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