@inproceedings{fa8e9ed32c0e48e4b068c28ff29ffca5,
title = "Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic",
abstract = "Step-indexed separation logic has proven to be a powerful tool for modular reasoning about higher-order stateful programs. However, it has only been used to reason about safety properties, never liveness properties. In this paper, we observe that the inability of step-indexed separation logic to support liveness properties stems fundamentally from its failure to validate the existential property, connecting the meaning of existential quantification inside and outside the logic. We show how to validate the existential property-and thus enable liveness reasoning-by moving from finite step-indices (natural numbers) to transfinite step-indices (ordinals). Concretely, we transform the Coq-based step-indexed logic Iris to Transfinite Iris, and demonstrate its effectiveness in proving termination and termination-preserving refinement for higher-order stateful programs.",
keywords = "Iris, Separation logic, liveness properties, ordinals, step-indexing, transfinite",
author = "Simon Spies and Lennard G{\"a}her and Daniel Gratzer and Joseph Tassarotti and Robbert Krebbers and Derek Dreyer and Lars Birkedal",
note = "Publisher Copyright: {\textcopyright} 2021 Owner/Author.; 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 ; Conference date: 20-06-2021 Through 25-06-2021",
year = "2021",
month = jun,
day = "18",
doi = "10.1145/3453483.3454031",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "80--95",
editor = "Freund, {Stephen N.} and Eran Yahav",
booktitle = "PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation",
}