Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic

Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal

doi:10.1145/3453483.3454031

Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic

Simon Spies
, Lennard Gäher
, Daniel Gratzer
, Joseph Tassarotti
, Robbert Krebbers
, Derek Dreyer
, Lars Birkedal

Department of Computer Science

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

29 Citations (Scopus)

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.

Original language	English
Title of host publication	PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Editors	Stephen N. Freund, Eran Yahav
Number of pages	16
Place of publication	New York
Publisher	Association for Computing Machinery
Publication date	Jun 2021
Pages	80-95
ISBN (Electronic)	9781450383912
DOIs	https://doi.org/10.1145/3453483.3454031
Publication status	Published - Jun 2021
Event	42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 - Virtual, Online, Canada Duration: 20 Jun 2021 → 25 Jun 2021

Conference

Conference	42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Country/Territory	Canada
City	Virtual, Online
Period	20/06/2021 → 25/06/2021

Keywords

Iris
liveness properties
ordinals
Separation logic
step-indexing
transfinite

Access to Document

10.1145/3453483.3454031Licence: CC BY

Library access?

Check availability with the Royal Danish Library

Cite this

Spies, S., Gäher, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D., & Birkedal, L. (2021). Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In S. N. Freund, & E. Yahav (Eds.), PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 80-95). Association for Computing Machinery. https://doi.org/10.1145/3453483.3454031

Spies, Simon ; Gäher, Lennard ; Gratzer, Daniel et al. / Transfinite Iris : Resolving an existential dilemma of step-indexed separation logic. PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. editor / Stephen N. Freund ; Eran Yahav. New York : Association for Computing Machinery, 2021. pp. 80-95

@inproceedings{c9e9d37233d04ef2991537f2e7bde82d,

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, liveness properties, ordinals, Separation logic, 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,

doi = "10.1145/3453483.3454031",

language = "English",

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",

publisher = "Association for Computing Machinery",

address = "United States",

}

Spies, S, Gäher, L, Gratzer, D, Tassarotti, J, Krebbers, R, Dreyer, D & Birkedal, L 2021, Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. in SN Freund & E Yahav (eds), PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, pp. 80-95, 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, Virtual, Online, Canada, 20/06/2021. https://doi.org/10.1145/3453483.3454031

Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. / Spies, Simon; Gäher, Lennard; Gratzer, Daniel et al.
PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ed. / Stephen N. Freund; Eran Yahav. New York: Association for Computing Machinery, 2021. p. 80-95.

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Transfinite Iris

T2 - 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021

AU - Spies, Simon

AU - Gäher, Lennard

AU - Gratzer, Daniel

AU - Tassarotti, Joseph

AU - Krebbers, Robbert

AU - Dreyer, Derek

AU - Birkedal, Lars

PY - 2021/6

Y1 - 2021/6

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

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

KW - Iris

KW - liveness properties

KW - ordinals

KW - Separation logic

KW - step-indexing

KW - transfinite

UR - https://www.scopus.com/pages/publications/85108917362

U2 - 10.1145/3453483.3454031

DO - 10.1145/3453483.3454031

M3 - Article in proceedings

AN - SCOPUS:85108917362

SP - 80

EP - 95

BT - PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

A2 - Freund, Stephen N.

A2 - Yahav, Eran

PB - Association for Computing Machinery

CY - New York

Y2 - 20 June 2021 through 25 June 2021

ER -

Spies S, Gäher L, Gratzer D, Tassarotti J, Krebbers R, Dreyer D et al. Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In Freund SN, Yahav E, editors, PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. New York: Association for Computing Machinery. 2021. p. 80-95 doi: 10.1145/3453483.3454031

Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic

Abstract

Conference

Keywords

Access to Document

Library access?

Other files and links

Fingerprint

Cite this