Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Andrés Aristizábal 1 Dariusz Biernacki 2 Sergueï Lenglet 3 Piotr Polesiuk 2
1 Pontificia Universidad Javeriana
2 Faculty of Mathematics and Computer Science [Wroclaw]
3 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.
Keywords : environmental bisimulation contextual equival- ence delimited continuation dynamic prompt generation up-to technique
Type de document :
Communication dans un congrès
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. 52, LIPIcs. 〈10.4230/LIPIcs.FSCD.2016.9〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01335959
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 22 juin 2016 - 15:06:55
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24

Fichier

LIPIcs-FSCD-2016-9.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Relations

Citation

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. 52, LIPIcs. 〈10.4230/LIPIcs.FSCD.2016.9〉. 〈hal-01335959〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

184

Téléchargements de fichiers

49

Contact


archive-ouverte@inria.fr