Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

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.
Type de document :
Rapport
[Research Report] RR-8905, Inria. 2016
Liste complète des métadonnées


https://hal.inria.fr/hal-01305137
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 30 août 2017 - 10:38:10
Dernière modification le : mercredi 20 septembre 2017 - 12:28:05

Fichier

RR-8905v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01305137, version 4

Collections

Relations

  • est un autre format de hal-01590620 - Corresponding journal paper

Citation

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. [Research Report] RR-8905, Inria. 2016. <hal-01305137v4>

Partager

Métriques

Consultations de
la notice

22

Téléchargements du document

11