| Autor: |
Aristizábal, Andrés, Biernacki, Dariusz, Lenglet, Sergueï, Polesiuk, Piotr |
| Rok vydání: |
2016 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Volume 13, Issue 3 (September 19, 2017) lmcs:2563 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.23638/LMCS-13(3:27)2017 |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
