License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2013.188
URN: urn:nbn:de:0030-drops-46320
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4632/
Ilik, Danko ;
Nakata, Keiko
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
Abstract
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one has to use a countable choice axiom in the proof and that Markov's Principle is replaceable by slightly strengthening the Double-negation Shift schema. We show that this strengthened version of Double-negation Shift can nonetheless be derived in a constructive intermediate logic based on delimited control operators, extended with axioms for higher-type Heyting Arithmetic. We formalize the argument and thus obtain a proof term that directly derives Open Induction on Cantor space by the shift and reset delimited control operators of Danvy and Filinski.
BibTeX - Entry
@InProceedings{ilik_et_al:LIPIcs:2014:4632,
author = {Danko Ilik and Keiko Nakata},
title = {{A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {188--201},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Ralph Matthes and Aleksy Schubert},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2014/4632},
URN = {urn:nbn:de:0030-drops-46320},
doi = {10.4230/LIPIcs.TYPES.2013.188},
annote = {Keywords: Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators}
}
Keywords: |
|
Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators |
Collection: |
|
19th International Conference on Types for Proofs and Programs (TYPES 2013) |
Issue Date: |
|
2014 |
Date of publication: |
|
25.07.2014 |