Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01590620
Contributor : Sergueï Lenglet <>
Submitted on : Tuesday, September 19, 2017 - 6:12:02 PM
Last modification on : Thursday, July 4, 2019 - 3:56:24 PM

Links full text

Identifiers

Collections

Relations

  • is format of hal-01335959 - Long version of the corresponding FSCD paper

Citation

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (3), ⟨10.23638/LMCS-13(3:27)2017⟩. ⟨hal-01590620⟩

Share

Metrics

Record views

419