一句话：在 Cubical Agda 中用商类型形式化带方程的代数效应，并提供效应通用的 Hoare 逻辑与等式推理。
本文关注带等式（equations）的代数效应在依赖类型论中的形式化。以往工作多借助 setoid 处理效应方程带来的商结构，而本文在 Cubical Agda 中改用商类型（quotient types）忠实编码按定律商去后的项。作者构建了一个库，既提供代数效应的等式推理工具，也给出一个效应通用的 Hoare 逻辑，使带效应程序可以按前置/后置条件进行推理。特别地，该工作通过 Hoare 逻辑的消去原理（elimination principle）将等式推理与 Hoare 风格推理联系起来。其贡献在于把高阶商类型、代数效应和 Hoare 逻辑统一在同一立方类型论框架中，从而支持对效应程序进行机器化验证与等式推导。评估主要是 Cubical Agda 中的形式化实现及其推理机制的关联性。
This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed setoids to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post-conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.
@article{paperbot2613,
title = {Algebraic Effects Meet Hoare Logic in Cubical Agda},
author = {Donnacha Oisín Kidney and Zhixuan Yang and Nicolas Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632898}
}