一句话：在 Coq 中形式化几何凸单子，为概率与非确定性选择的等式推理提供可信模型和可复用理论。
概率选择与非确定性选择的代数性质长期是程序语义研究主题。本文在 Coq 证明助手中形式化同时包含两种选择的几何凸单子（geometrically convex monad）。该形式化为一个实现非平凡接口的单子提供模型，使得可用等式推理证明带概率与非确定性效果的程序性质。作者阐述从文献到完整 Coq 形式化的技术选择，提炼凸空间、具体范畴等数学结构的可复用理论，并将其集成到单子等式推理框架中。
Abstract The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a nontrivial interface, which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.
@article{paperbot1229,
title = {A trustful monad for axiomatic reasoning with probability and nondeterminism},
author = {REYNALD AFFELDT and JACQUES GARRIGUE and DAVID NOWAK and TAKAFUMI SAIKAWA},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796821000137}
}