一句话：提出首个用于证明高阶并发概率程序上下文精化的高阶分离逻辑 Foxtrot，并在 Rocq/Iris 中机器化验证。
本文研究如何证明带高阶局部状态的高阶并发概率程序的上下文精化。现有并发分离逻辑难以同时处理概率与并发。作者提出 Foxtrot：一种高阶分离逻辑，继承不变式、幽灵资源等并发推理原则，并支持 tape presampling、误差放大归纳等概率推理原则，用以分析并发线程诱导的复杂概率分布。逻辑可靠性在 Iris 中依赖一版选择公理，概率与并发的融合使其模型与证明高度非平凡。作者在对抗性 von Neumann 硬币及 Sodium 密码库的 randombytes_uniform 等例子上展示表达力，所有结果已在 Rocq 与 Iris 中机器化。
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the randombytes _ uniform function of the Sodium cryptography software library. All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LiATB26,
title = {Contextual Refinement of Higher-Order Concurrent Probabilistic Programs},
author = {Kwing Hei Li and Alejandro Aguirre and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808265}
}