Skip to Main content Skip to Navigation
Conference papers

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 :
Conference papers
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-01335959
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, June 22, 2016 - 3:06:55 PM
Last modification on : Saturday, November 21, 2020 - 9:54:03 AM

File

LIPIcs-FSCD-2016-9.pdf
Publisher files allowed on an open archive

Identifiers

Collections

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. ⟨10.4230/LIPIcs.FSCD.2016.9⟩. ⟨hal-01335959⟩

Share

Metrics

Record views

236

Files downloads

115