摘要：We present sound and complete environmental bisimilarities for a variant ofDybvig et al.'s calculus of multi-prompted delimited-control operators withdynamic prompt generation. The reasoning principles that we obtain generalizeand advance the existing techniques for establishing program equivalence incalculi with single-prompted delimited control. The basic theory that wedevelop is presented using Madiot et al.'s framework that allows for smoothintegration and composition of up-to techniques facilitating bisimulationproofs. We also generalize the framework in order to express environmentalbisimulations that support equivalence proofs of evaluation contextsrepresenting continuations. This change leads to a novel and powerful up-totechnique enhancing bisimulation proofs in the presence of control operators.
