Aarhus University Seal / Aarhus Universitets segl

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

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

  • Simon Spies, Saarland University, Max Planck Institute for Software Systems
  • ,
  • Lennard Gäher, Max Planck Institute for Software Systems, Saarland University
  • ,
  • Daniel Gratzer
  • Joseph Tassarotti, Boston College
  • ,
  • Robbert Krebbers, Radboud University Nijmegen
  • ,
  • Derek Dreyer, Max Planck Institute for Software Systems
  • ,
  • Lars Birkedal

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 languageEnglish
Title of host publicationPLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsStephen N. Freund, Eran Yahav
Number of pages16
Place of publicationNew York
PublisherAssociation for Computing Machinery
Publication yearJun 2021
Pages80-95
ISBN (Electronic)9781450383912
DOIs
Publication statusPublished - Jun 2021
Event42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 - Virtual, Online, Canada
Duration: 20 Jun 202125 Jun 2021

Conference

Conference42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
LandCanada
ByVirtual, Online
Periode20/06/202125/06/2021
SponsorACM SIGPLAN

Bibliographical note

Publisher Copyright:
© 2021 Owner/Author.

    Research areas

  • Iris, liveness properties, ordinals, Separation logic, step-indexing, transfinite

See relations at Aarhus University Citationformats

ID: 224101633