Confluence for classical logic through the distinction between values and computations

MaRDI QIDQ4995381zbMATH OpenFDO

Authors José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto

Publication date 24 June 2021

Full work available at URL https://arxiv.org/abs/1409.3316, http://eptcs.web.cse.unsw.edu.au/paper.cgi?CLaC14.5

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• On semantics of a term calculus for classical logic
• Call-by-name reduction and cut-elimination in classical logic
• Free deduction: An analysis of ``computations in classical logic
• Cut elimination for classical proofs as continuation passing style computation
• Monadic translation of classical sequent calculus

This page was built for publication: Confluence for classical logic through the distinction between values and computations

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