Bisimulations for Delimited-Control Operators
Logic in Computer Science
2023-06-22 v4
Abstract
We present a comprehensive study of the behavioral theory of an untyped -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.
Keywords
Cite
@article{arxiv.1804.08373,
title = {Bisimulations for Delimited-Control Operators},
author = {Dariusz Biernacki and Sergueï Lenglet and Piotr Polesiuk},
journal= {arXiv preprint arXiv:1804.08373},
year = {2023}
}