一句话：给出非确定性、概率与终止组合所得 monad 的呈现，提供程序等价性与距离的等式推理工具。
在程序语义中，非确定性、概率行为与终止可能性常常需要同时刻画，但为这些组合行为提供统一的代数推理工具并不容易。本文研究由非确定性与概率行为结合终止可能性所产生的 monad，并给出这些 monad 的 presentation 结果，即用生成元与等式公理系统来刻画它们。借助这些 presentation，作者为程序语义提供了等式推理工具，可用于证明程序之间的等价性；同时也在度量层面支持程序间距离的推理。论文的主要贡献是理论性的 presentation 结果，摘要未涉及具体实现或实验评估。
We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.
DOI 原文 ·
@inproceedings{paperbot6237,
title = {Combining Nondeterminism, Probability, and Termination: Equational and Metric Reasoning},
author = {Matteo Mio and Ralph Sarkis and Valeria Vignudelli},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470717}
}