Reference. The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic

Cite

Cite as @vindum-2025-the (helia, typst) · \cite{vindum-2025-the} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{vindum-2025-the, series={CPP ’25}, title={The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic}, url={http://dx.doi.org/10.1145/3703595.3705876}, DOI={10.1145/3703595.3705876}, booktitle={Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs}, publisher={ACM}, author={Vindum, Simon Friis and Georges, Aïna Linn and Birkedal, Lars}, year={2025}, month=Jan, pages={83–97}, collection={CPP ’25} }
hayagriva YAML (typst)
yaml · 19 lines
vindum-2025-the:
  type: article
  title: 'The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic'
  author:
  - Vindum, Simon Friis
  - Georges, Aïna Linn
  - Birkedal, Lars
  date: 2025-01
  page-range: 83-97
  url: http://dx.doi.org/10.1145/3703595.3705876
  serial-number:
    doi: 10.1145/3703595.3705876
  parent:
    type: proceedings
    title: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs
    publisher: ACM
    parent:
      type: proceedings
      title: CPP ’25
Cited by (1)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants zilberstein-2026-probabilistic

Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
PDF · DOI · arXiv · pldb
Cites 20 works (5 here)
With notes (5)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic spies-2021-transfinitex

PDF · DOI · pldb

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_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

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST timany-2017-a

We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.
PDF · DOI · pldb

Interactive proofs in higher-order concurrent separation logic krebbers-2017-interactive

PDF · DOI · pldb

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-iris

PDF · DOI · pldb
vindum-2025-the reference entries/refs/vindum-2025-the/vindum-2025-the.hel