一句话：提出首个高阶并发概率程序错误概率界推理的分离逻辑 Coneris，支持随机化逻辑原子性并由 Rocq/Iris 机器化验证。
论文针对高阶并发概率程序缺少模块化推理错误概率界的问题，提出 Coneris——首个面向此类程序的高阶并发分离逻辑。它把经典线性化思想内化到逻辑中，并扩展为随机化逻辑原子性，以支持并发概率模块的模块化推理；为此引入预采样带（presampling tapes）和新的概率更新模态，在性线化点描述状态的概率性变化。作者通过小型合成例子和较大案例研究展示方法，并在 Rocq 证明助手与 Iris 分离逻辑框架中机器化验证了全部结果，包括元理论。
We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity . In Coneris, we extend this idea to probabilistic concurrent program modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq prover and the Iris separation logic framework.
@article{paperbot3045,
title = {Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs},
author = {Kwing Hei Li and Alejandro Aguirre and Simon Oddershede Gregersen and Philipp G. Haselwarter and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747514}
}