Andrés Aristizábal ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk - Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

lmcs:2563 - Logical Methods in Computer Science, September 19, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:27)2017
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt GenerationArticle

Authors: Andrés Aristizábal ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk

    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.


    Volume: Volume 13, Issue 3
    Published on: September 19, 2017
    Accepted on: September 1, 2017
    Submitted on: May 2, 2017
    Keywords: Computer Science - Programming Languages

    1 Document citing this article

    Consultation statistics

    This page has been seen 1297 times.
    This article's PDF has been downloaded 415 times.