一句话：提出首个可为任意单子效应定义关系程序逻辑的通用框架，并给出语义基础与可靠逻辑核心。
本文研究如何统一地为任意单子效应建立语义可靠的关系程序逻辑，并解决既有工作难以处理控制效应的问题。作者在关系依赖类型论中嵌入该框架，语义上用 relative monads 代数地表示关系规约，并引入关系效应观察（relational effect observations），在保持代数结构的前提下把单子计算对映射为关系规约。对任意关系效应观察，框架可泛型地定义可靠关系程序逻辑的核心，并可扩展为面向具体效应的完整逻辑。作者为状态、输入输出、非确定性和离散概率等效应定义了相应逻辑，还用状态与无界迭代嵌入 Benton 关系霍尔逻辑的变体并重构关系霍尔类型论，且首次给出异常的关系程序逻辑。
We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare Logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions.
@article{paperbot518,
title = {The next 700 relational program logics},
author = {Kenji Maillard and Cătălin Hriţcu and Exequiel Rivas and Antoine Van Muylder},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371072}
}