一句话：提出以自由单子与处理器分层构建抽象解释器，并在 Coq 中模块化验证其可靠性。
本文研究如何在 Coq 等依赖类型理论中实现并验证抽象解释器。作者采用 ITree 等库倡导的方法，把单子解释器组织为堆叠在自由单子上的处理器层，以复用代码并模块化证明可靠性。文中给出通用抽象控制流组合子，一次性证明其相对具体对应物的正确性；说明如何关联实现效应的具体与抽象处理器，以在单子解释器语境下刻画转移函数的传统可靠性；并提供通过状态与失败效应解释提升可靠性陈述的通用结果。相关理论在 Coq 库中形式化，并用结构化命令式语言和玩具汇编两个示例抽象解释器验证。
We argue that monadic interpreters built as layers of handlers stacked atop the free monad, as advocated notably by the ITree library, also constitute a promising way to implement and verify abstract interpreters in dependently-typed theories such as the one underlying the Coq proof assistant. The approach enables both code reuse across projects and modular proofs of soundness of the resulting interpreters. We provide generic abstract control flow combinators proven correct once and for all against their concrete counterpart. We demonstrate how to relate concrete handlers implementing effects to abstract variants of these handlers, essentially capturing the traditional soundness of transfer functions in the context of monadic interpreters. Finally, we provide generic results to lift soundness statements via the interpretation of stateful and failure effects. We formalize all the aforementioned combinators and theories into a Coq library, and demonstrate their benefits by implementing and proving correct two illustrative abstract interpreters respectively for a structured imperative language and a toy assembly.
@article{MichellandZG24,
title = {Abstract Interpreters: A Monadic Approach to Modular Verification},
author = {Sébastien Michelland and Yannick Zakowski and Laure Gonnord},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674646}
}