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
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
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.
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

article.pdf
Publisher files allowed on an open archive

Identifiers

Collections

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⟩

Share

Metrics

Record views

528

Files downloads

353