The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express---and invariants enable us to enforce---user-defined *protocols* on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a *view shift*, Iris supports the encoding of *logically atomic specifications*, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not.
@misc{jung2015iris,
title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning},
author = {Ralf Jung and David Swasey and Filip Sieczkowski and Kasper Svendsen and Aaron Joseph Turon and Lars Birkedal and Derek R. Dreyer},
year = {2015},
journal = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
pages = {637--650},
doi = {10.1145/2676726.2676980},
}
This record lives at https://refs.drheap.org/jung2015iris/ and will keep
doing so. It used to be called jung2014iris, and those addresses still resolve to this one.