Simon Spies, Lennard GĂ¤her, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

*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.