一句话：为支持动态提示生成的多提示定界控制演算提出可靠且完备的环境互模拟，并给出新的 up-to 证明技术。
本文研究带动态提示生成的多提示定界控制算子演算中的程序等价性，该演算扩展了 Dybvig 等人的工作。作者提出可靠且完备的环境互模拟，将单提示定界控制的现有推理原则推广到多提示与动态生成提示的情形。基本理论基于 Madiot 等人的框架，便于 up-to 技术的整合与组合，从而简化互模拟证明。作者进一步扩展该框架，使环境互模拟能够证明表示续延的求值上下文之间的等价。这一扩展产生了一种新颖且强大的 up-to 技术，增强了存在控制算子时的互模拟证明能力。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AristizabalBLP16,
title = {Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation},
author = {Andrés Aristizábal and Dariusz Biernacki and Sergueï Lenglet and Piotr Polesiuk},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:27)2017}
}