一句话：为带 shift/reset 的无类型 λ 演算定义上下文等价，并在统一框架中用多种互模拟刻画其行为理论。
论文系统研究带定界控制算子 shift 和 reset 的无类型 λ 演算的行为理论。作者首先为该演算定义上下文等价，并试图用余归纳定义的互模拟关系来刻画它。文章在一个统一框架内考察 applicative、normal-form 和环境式（environmental）三种互模拟风格，通过实例比较它们各自的表达能力、优点与局限。该工作为定界控制算子的程序等价与行为推理提供语义基础，并讨论如何将方法扩展到其他定界控制算子。
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.
@article{paperbot789,
title = {Bisimulations for Delimited-Control Operators},
author = {Dariusz Biernacki and Sergueï Lenglet and Piotr Polesiuk},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:18)2019}
}