一句话：提出 Kripke 范式双模拟，用操作博弈语义统一四类高阶语言的上下文等价关系推理，并证明其可靠完备。
论文提出以操作博弈语义为指南，为四类 call-by-value 高阶语言建立上下文等价的关系推理技术。这四类语言分别覆盖一般引用/基础类型引用以及 call/cc/无控制算子的组合。作者定义 Kripke 范式双模拟，将范式双模拟与 Kripke 逻辑关系同博弈语义结合，用 Kripke 风格世界迁移系统抽象堆与名字历史；四类上下文的差异通过局部条件体现，并对应 O-visibility 与 O-bracketing。该技术相对于操作博弈语义是可靠且完备的，并重新解释了 Kripke 逻辑关系中的回溯与私有迁移等现象。
We show how to use operational game semantics as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages: with either general or ground-type references and with either call/cc or no control operator. In game semantics, differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.The proposed technique, which we call Kripke normal-form bisimulations, combines insights from normal-form bisimulation and Kripke logical relations with game semantics. In particular, the role of the heap and the name history is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, as applicable.The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, it sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.
DOI 原文 ·
@inproceedings{paperbot6235,
title = {Compositional relational reasoning via operational game semantics},
author = {Guilhem Jaber and Andrzej S. Murawski},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470524}
}