Reference. Transfinite step-indexing for termination

Simon Spies, Neel Krishnaswami, Derek Dreyer · POPL · 2021 · logical-relations · PDF · DOI · pldb
Step-indexed logical relations are an extremely useful technique for building operational-semantics-based models and program logics for realistic, richly-typed programming languages. They have proven to be indispensable for modeling features like higher-order state , which many languages support but which were difficult to accommodate using traditional denotational models. However, the conventional wisdom is that, because they only support reasoning about finite traces of computation, (unary) step-indexed models are only good for proving safety properties like “well-typed programs don’t go wrong”. There has consequently been very little work on using step-indexing to establish liveness properties, in particular termination. In this paper, we show that step-indexing can in fact be used to prove termination of well-typed programs—even in the presence of dynamically-allocated, shared, mutable, higher-order state—so long as one’s type system enforces disciplined use of such state. Specifically, we consider a language with asynchronous channels, inspired by promises in JavaScript, in which higher-order state is used to implement communication, and linearity is used to ensure termination. The key to our approach is to generalize from natural number step-indexing to transfinite step-indexing , which enables us to compute termination bounds for program expressions in a compositional way. Although transfinite step-indexing has been proposed previously, we are the first to apply this technique to reasoning about termination in the presence of higher-order state.

Cite
Cite as @spies-2021-transfinite (helia, typst) · \cite{spies-2021-transfinite} (LaTeX)
BibTeX
bibtex · 1 line
@article{spies-2021-transfinite, title={Transfinite step-indexing for termination}, volume={5}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3434294}, DOI={10.1145/3434294}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Spies, Simon and Krishnaswami, Neel and Dreyer, Derek}, year={2021}, month=Jan, pages={1–29} }
hayagriva YAML (typst)
yaml · 19 lines
spies-2021-transfinite:
  type: article
  title: Transfinite step-indexing for termination
  author:
  - Spies, Simon
  - Krishnaswami, Neel
  - Dreyer, Derek
  date: 2021-01
  page-range: 1-29
  url: http://dx.doi.org/10.1145/3434294
  serial-number:
    doi: 10.1145/3434294
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 5
Download: spies-2021-transfinite.bib · spies-2021-transfinite.yml
Cited by (2)

From Linearity to Borrowing wagner-2025-fromOOPSLA · 2025
Linear type systems are powerful because they can statically ensure the correct management of resources like memory, but they can also be cumbersome to work with, since even benign uses of a resource require that it be explicitly threaded through during computation. Borrowing , as popularized by Rust, reduces this burden by allowing one to temporarily disable certain resource permissions (e.g., deallocation or mutation) in exchange for enabling certain structural permissions (e.g., weakening or contraction). In particular, this mechanism spares the borrower of a resource from having to explicitly return it to the lender but nevertheless ensures that the lender eventually reclaims ownership of the resource. In this paper, we elucidate the semantics of borrowing by starting with a standard linear type system for ensuring safe manual memory management in an untyped lambda calculus and gradually augmenting it with immutable borrows, lexical lifetimes, reborrowing, and finally mutable borrows. We prove semantic type soundness for our Borrow Calculus ( BoCa ) using Borrow Logic ( BoLo ), a novel domain-specific separation logic for borrowing. We establish the soundness of this logic using a semantic model that additionally guarantees that our calculus is terminating and free of memory leaks. We also show that our Borrow Logic is robust enough to establish the semantic safety of some syntactically ill-typed programs that temporarily break but reestablish invariants.
PDF · DOI · pldb

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic spies-2021-transfinitexPLDI · 2021
PDF · DOI · pldb
Cites 40 works (2 here)
With notes (2)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018JFP · 2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
PDF · DOI · pldb

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-irisPOPL · 2015
PDF · DOI · pldb
External (38)
spies-2021-transfinite reference entries/refs/spies-2021-transfinite/spies-2021-transfinite.hel