Continuation-passing Style Models Complete for Intuitionistic Logic

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 : A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a $\beta$-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvy's type-directed partial evaluator for the same lambda calculus, the there essential use of delimited control operators (i.e. computational effects) is avoided. The role of polymorphism is crucial -- dropping it allows one to obtain a notion of model complete for classical predicate logic. The connection between ours and Kripke models is made through a strengthening of the Double-negation Shift schema.
Type de document :
Article dans une revue
Annals of Pure and Applied Logic, Elsevier Masson, 2012, <10.1016/j.apal.2012.05.003>
Liste complète des métadonnées


https://hal.inria.fr/hal-00647390
Contributeur : Danko Ilik <>
Soumis le : mercredi 9 mai 2012 - 10:01:54
Dernière modification le : jeudi 9 février 2017 - 15:17:21
Document(s) archivé(s) le : vendredi 10 août 2012 - 02:22:52

Fichiers

intcomp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Danko Ilik. Continuation-passing Style Models Complete for Intuitionistic Logic. Annals of Pure and Applied Logic, Elsevier Masson, 2012, <10.1016/j.apal.2012.05.003>. <hal-00647390v3>

Partager

Métriques

Consultations de
la notice

368

Téléchargements du document

248