一句话：在 Coq 中以接口方式形式化效应单子层级与代数律，使单子等式推理可机器化并实用化。
该论文关注带计算效应程序的等式推理虽可由单子支持，但大规模纸笔证明难以维护，缺乏实用形式化框架。作者在 Coq 证明助手中提出一种效应层级的形式化方法：把效应层级与代数律组织为类似依赖类型论中代数层级接口的模块接口，从而清晰分离等式律与具体模型。该方法利用 Coq 的复杂重写能力和引理库实现简洁证明，并借助 Coq 数学理论形式化单子模型。文中形式化了非确定性、状态、概率等丰富效应层级，机器化了文献中的多个单子等式推理实例，并将该框架用于为带引用的 ML 子集设计等式律。
Abstract One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent-type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq’s mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AffeldtGS25,
title = {A practical formalization of monadic equational reasoning in dependent-type theory},
author = {REYNALD AFFELDT and JACQUES GARRIGUE and TAKAFUMI SAIKAWA},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796824000157}
}