Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
复制标题
高阶分离逻辑中的异步概率耦合
DOI：
10.1145/3632868
复制
发表时间：
2024
影响因子：
--
通讯作者：
Birkedal, Lars
中科院分区：
文献类型：
--
作者：
Gregersen, Simon Oddershede;Aguirre, Alejandro;Haselwarter, Philipp G.;Tassarotti, Joseph;Birkedal, Lars
概率耦合是许多概率关系程序逻辑的基础，并且在两个程序之间关联随机采样语句时出现。在关系程序逻辑中，这表现为专用的耦合规则，例如，我们可以推理好像两个采样语句返回相同的值。然而，这种方法从根本上需要对齐或“同步”两个程序的采样语句，而这并不总是可能的。在本文中，我们开发了 Clutch，一种高阶概率关系分离逻辑，它通过支持异步概率耦合来解决这个问题。我们使用 Clutch 开发逻辑步骤索引逻辑关系，以推理用具有概率选择运算符、高阶局部状态和命令多态性的丰富语言编写的高阶程序的上下文细化和等价性。最后，我们在一些案例研究中展示了我们的方法。论文中出现的所有结果都已使用 Coquelicot 库和 Iris 分离逻辑框架在 Coq 证明助手中形式化。
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.
登录
查看更多内容
混合论证概述摘自：哈希函数和随机预言的理论 - 现代密码学的一种方法
DOI：
--
发表时间：
2021
期刊：
影响因子：
--
作者：
M. Fischlin;Arno Mittelbach
通讯作者：
Arno Mittelbach
影响因子：
0.8
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
通讯作者：
Melquiond, Guillaume
DOI：
--
发表时间：
2019
期刊：
IEEE Symposium on Security and Privacy
影响因子：
--
作者：
D. Frumin;Robbert Krebbers;L. Birkedal
通讯作者：
L. Birkedal
影响因子：
0.6
作者：
Dreyer, Derek;Ahmed, Amal;Birkedal, Lars
通讯作者：
Birkedal, Lars
DOI：
10.1007/s10817-020-09545-0
发表时间：
2020-02-08
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Eberl, Manuel;Haslbeck, Max W.;Nipkow, Tobias
通讯作者：
Nipkow, Tobias