一句话：提出 later credits，将“消除 later 的权利”变为分离逻辑可拥有资源，以突破 later 模态证明困境。
过去二十年，步进索引逻辑关系与分离逻辑在语义和验证研究中作用重大；VST、iCAP、Iris 等步进索引分离逻辑将二者结合，用步进索引模型解释命题，并通过“later”模态将步进推理反映到逻辑中。later 模态提供了优雅的高层步进推理，但在足够复杂的证明中，它会把自然策略变成死胡同。本文提出 later credits：把“消除一个 later 的权利”变成可由分离逻辑拥有的资源，从而可像普通资源一样遵循分离逻辑的模块化推理原则。作者在 Iris 语境中发展该理论，并给出若干此前无法在 Iris 中完成或不自然的困难证明与证明模式，表明 later credits 能有效规避 later 模态困境。
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.
@article{paperbot1479,
title = {Later credits: resourceful reasoning for the later modality},
author = {Simon Spies and Lennard Gäher and Joseph Tassarotti and Ralf Jung and Robbert Krebbers and Lars Birkedal and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547631}
}