Skip to Main content Skip to Navigation
Journal articles

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators

Danko Ilik 1, * Keiko Nakata 2
* Corresponding author
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01092427
Contributor : Danko Ilik <>
Submitted on : Monday, December 8, 2014 - 4:34:43 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Monday, March 9, 2015 - 12:11:00 PM

File

11.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Danko Ilik, Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. Leibniz International Proceedings in Informatics , Leibniz-Zentrum für Informatik, 2014, pp.288-201. ⟨10.4230/LIPIcs.TYPES.2013.188⟩. ⟨hal-01092427⟩

Share

Metrics

Record views

491

Files downloads

160