一句话：提出用模态逻辑刻画代数效应程序行为等价的一般框架，并证明其与applicative bisimilarity一致且为同余。
本文研究带代数效应触发操作的值调用函数式语言中程序的行为等价。作者定义一种逻辑，其公式描述行为性质，核心是一组表达效应特定行为的模态，并给出模态的一般理论。若模态满足 openness 和 decomposability 两个条件，则逻辑定义的行为等价与模态定义的 applicative bisimilarity 重合；借助 Howe 方法的推广，可证明后者是同余关系。作者验证非确定性、概率选择、全局存储及输入/输出等效应实例均满足这两个条件，从而提供统一的行为等价证明框架。
The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities, then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store, and input/output.
@article{paperbot698,
title = {Behavioural Equivalence via Modalities for Algebraic Effects},
author = {Alex Simpson and Niels Voorneveld},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {1},
year = {2019},
doi = {10.1145/3363518}
}