The Peirce translation and the double negation shift

DOI10.1007/978-3-642-13962-8_17MaRDI QIDQ3576201zbMATH OpenOpenAlexFDO

Authors Martín Escardo, Paulo Oliva

Publication date 29 July 2010

Published in Programs, Proofs, Processes (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-13962-8_17

zbMATH Keywords

countable choiceminimal logiccomputational extraction of witnesses from proofs in classical analysisdependent choicefunctional interpretationmodified realizabilitynegative translationselection functionsdouble-negation shiftPeirce translation

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07) Functionals in proof theory (03F10)

Recommendations

• The Peirce translation
• scientific article; zbMATH DE number 6307933
• scientific article; zbMATH DE number 2185652
• Refinement of classical proofs for program extraction
• A New Translation for Semi-classical Theories — Backtracking without CPS

Cited in

(9)

• scientific article; zbMATH DE number 6307933 (Why is no real title available?)
• Higher-order games with dependent types
• Double negation semantics for generalisations of Heyting algebras
• The Peirce translation
• The Herbrand functional interpretation of the double negation shift
• scientific article; zbMATH DE number 7447766 (Why is no real title available?)
• scientific article; zbMATH DE number 7204446 (Why is no real title available?)
• Delimited control operators prove double-negation shift
• Negative Translations and Duality: Toward a Unified Approach

This page was built for publication: The Peirce translation and the double negation shift

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