Later credits: resourceful reasoning for the later modality
Later credits: resourceful reasoning for the later modality
复制标题
后期学分：对后期模式的机智推理
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Derek Dreyer
中科院分区：
文献类型：
--
作者：
Simon Spies;Lennard Gäher;Joseph Tassarotti;Ralf Jung;R. Krebbers;L. Birkedal;Derek Dreyer
在过去的二十年里，阶梯索引逻辑关系和分离逻辑在语义和验证研究中都发挥了重要作用。最近，它们以步进索引分离逻辑的形式结合在一起，如VST、iCAP和Iris，它们为（除其他外）构建类型丰富的语言（如Rust）的语义模型提供了强大的工具。在这些逻辑中，使用阶梯索引模型赋予命题语义，阶梯索引推理通过所谓的“后”模态反映到逻辑中。一方面，这种模式提供了一种优雅的、高层次的阶梯索引推理；另一方面，当以足够复杂的方式使用时，它可能会成为一种麻烦，将完美的自然证明策略变成死胡同。在这项工作中，我们介绍了后期信用，这是一种逃避后模态泥潭的新技术。通过利用这些逻辑的第二个祖先——分离逻辑，后来者信用将“消除后来者的权利”变成了一种可拥有的资源，它服从于分离逻辑的所有传统模块化推理原则。我们在Iris的背景下发展了后期学分理论，并提出了几个具有挑战性的证明和证明模式的例子，这些例子以前在Iris中是不可能的，但现在由于后期学分而成为可能。
In the past two decades, step-indexed logical relations and separation logics have both come to play a major role in semantics and verification research. More recently, they have been married together in the form of step-indexed separation logics like VST, iCAP, and Iris, which provide powerful tools for (among other things) building semantic models of richly typed languages like Rust. In these logics, propositions are given semantics using a step-indexed model, and step-indexed reasoning is reflected into the logic through the so-called “later” modality. On the one hand, this modality provides an elegant, high-level account of step-indexed reasoning; on the other hand, when used in sufficiently sophisticated ways, it can become a nuisance, turning perfectly natural proof strategies into dead ends. In this work, we introduce later credits, a new technique for escaping later-modality quagmires. By leveraging the second ancestor of these logics—separation logic—later credits turn “the right to eliminate a later” into an ownable resource, which is subject to all the traditional modular reasoning principles of separation logic. We develop the theory of later credits in the context of Iris, and present several challenging examples of proofs and proof patterns which were previously not possible in Iris but are now possible due to later credits.
登录
查看更多内容
DOI：
10.4230/lipics.itp.2021.32
发表时间：
2021
期刊：
--
影响因子：
--
作者：
Hengchu Zhang;Wolf Honoré;Nicolas C. H. Koh;Yao Li;Yishuai Li;Li-yao Xia;Lennart Beringer;William Mansky;B. Pierce;Steve Zdancewic
通讯作者：
Hengchu Zhang;Wolf Honoré;Nicolas C. H. Koh;Yao Li;Yishuai Li;Li-yao Xia;Lennart Beringer;William Mansky;B. Pierce;Steve Zdancewic
不受分离逻辑规范影响的定理
影响因子：
--
作者：
Birkedal L
通讯作者：
Birkedal L
使用 Perennial 验证并发、防碰撞系统
DOI：
10.1145/3341301.3359632
发表时间：
2019
期刊：
Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP
影响因子：
--
作者：
Chajed, Tej;Tassarotti, Joseph;Kaashoek, Frans;Zeldovich, Nickolai
通讯作者：
Zeldovich, Nickolai
递归世界上的阶跃索引克里普克模型
影响因子：
--
作者：
Birkedal L
通讯作者：
Birkedal L