HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata
https://hal.inria.fr/hal-00647389
Contributor : Danko Ilik Connect in order to contact the contributor
Submitted on : Friday, December 2, 2011 - 12:21:27 AM
Last modification on : Friday, January 21, 2022 - 3:21:52 AM
Long-term archiving on: : 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-LIX | X | PPS | INRIA2 | X-DEP-INFO | UNIV-PARIS7 | UNIV-PARIS

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 Datacite

Share

Metrics

Record views

528

Files downloads

353

 

Contact                    Legal Notice                    Personal Data