Skip to Main content Skip to Navigation
Journal articles

Delimited control operators prove Double-negation Shift

Danko Ilik 1, 2, 3
1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
3 PPS - Preuves, Programmes et Systèmes
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.
Document type :
Journal articles
Complete list of metadatas
https://hal.inria.fr/hal-00647389
Contributor : Danko Ilik <>
Submitted on : Friday, December 2, 2011 - 12:21:27 AM
Last modification on : Friday, March 27, 2020 - 3:07:01 AM
Document(s) archivé(s) le : Saturday, March 3, 2012 - 2:25:07 AM

Files

Vignette du document
article.pdf
Publisher files allowed on an open archive

Identifiers

Collections

CNRS | INRIA | LIX | INSMI | X | X-LIX | PPS | X-DEP-INFO | UNIV-PARIS7 | USPC

Citation

Danko Ilik. Delimited control operators prove Double-negation Shift. Annals of Pure and Applied Logic, Elsevier Masson, 2012, Kurt Goedel Research Prize Fellowships 2010, 163 (11), pp.1549-1559. ⟨10.1016/j.apal.2011.12.008⟩. ⟨hal-00647389⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

1154

Files downloads

895

 

Contact                    Legal Notice                    Personal Data