文章基本信息

标题：Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
本地全文：下载
作者：Andr{\'e}s Aristiz{\'a}bal ; Dariusz Biernacki ; Serguei Lenglet 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：52
页码：9:1-9:17
DOI：10.4230/LIPIcs.FSCD.2016.9
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：delimited continuation; dynamic prompt generation; contextual equivalence; environmental bisimulation; up-to technique