一句话：提出支持异步概率耦合的高阶概率关系分离逻辑 Clutch，并用于证明高阶程序的上下文精化与等价。
概率耦合是概率关系程序逻辑的基础，用于关联两个程序中的随机采样。但现有耦合规则通常要求同步对齐采样语句，当程序结构不同或无法同步时失效。本文提出 Clutch：一种支持异步概率耦合的高阶概率关系分离逻辑。基于 Clutch，作者建立了步进索引的逻辑关系，用于证明具有概率选择、高阶局部状态和不可预测多态的语言中程序的上下文精化与等价。论文通过多个案例研究展示方法有效性，并在 Coq 中用 Coquelicot 与 Iris 框架机器化验证了所有结果。
Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g ., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or “synchronizing” the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.
@article{paperbot2623,
title = {Asynchronous Probabilistic Couplings in Higher-Order Separation Logic},
author = {Simon Oddershede Gregersen and Alejandro Aguirre and Philipp G. Haselwarter and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632868}
}