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

Danko Ilik 1, * Keiko Nakata 2
* Auteur correspondant
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Article dans une revue
Leibniz International Proceedings in Informatics (LIPIcs), 2014, pp.288-201. 〈10.4230/LIPIcs.TYPES.2013.188〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01092427
Contributeur : Danko Ilik <>
Soumis le : lundi 8 décembre 2014 - 16:34:43
Dernière modification le : jeudi 12 avril 2018 - 01:49:26
Document(s) archivé(s) le : lundi 9 mars 2015 - 12:11:00

Fichier

11.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

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 (LIPIcs), 2014, pp.288-201. 〈10.4230/LIPIcs.TYPES.2013.188〉. 〈hal-01092427〉

Partager

Métriques

Consultations de la notice

210

Téléchargements de fichiers

93