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.
Type de document :
Article dans une revue
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>
Liste complète des métadonnées

https://hal.inria.fr/hal-00647389
Contributeur : Danko Ilik <>
Soumis le : vendredi 2 décembre 2011 - 00:21:27
Dernière modification le : jeudi 9 février 2017 - 15:17:17
Document(s) archivé(s) le : samedi 3 mars 2012 - 02:25:07

Fichiers

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

Identifiants

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>

Partager

Métriques

Consultations de
la notice

576

Téléchargements du document

286