Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk - Bisimulations for Delimited-Control Operators

lmcs:4458 - Logical Methods in Computer Science, May 24, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:18)2019
Bisimulations for Delimited-Control OperatorsArticle

Authors: Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk

    We present a comprehensive study of the behavioral theory of an untyped $\lambda$-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and environmental) within a unifying framework, and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.


    Volume: Volume 15, Issue 2
    Published on: May 24, 2019
    Accepted on: May 22, 2019
    Submitted on: April 24, 2018
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1100 times.
    This article's PDF has been downloaded 1038 times.