Delimited control operators prove Double-negation Shift
arXiv:1012.0929 · doi:10.1016/j.apal.2011.12.008
Abstract
We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the Double-negation Shift schema, while preserving the disjunction and existence properties.
References in corpus (2)
Cited by in corpus (7)
- Continuation-passing Style Models Complete for Intuitionistic Logic
- The Principle of Open Induction on Cantor space and the Approximate-Fan Theorem
- Type Directed Partial Evaluation for Level-1 Shift and Reset
- An interpretation of the Sigma-2 fragment of classical Analysis in System T
- An Intuitionistic Formula Hierarchy Based on High-School Identities
- A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
- Perspectives for proof unwinding by programming languages techniques