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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Country/TerritoryCanada
CityVirtual, Online
Period6/20/216/25/21

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this