[Iris-Club] Iris 3.4 and std++ 1.5
Ralf Jung
jung at mpi-sws.org
Wed Feb 17 10:02:56 CET 2021
Hello everyone,
we are happy to announce the release of Iris 3.4 and std++ 1.5. Iris is a
concurrent separation logic framework for Coq; for an overview of the numerous
research projects employing Iris, see <https://iris-project.org/>. Iris has a
logo now, so even if you checked out this website before, it's worth another
look. :)
std++ is an extended "standard" library for Coq.
The highlights and most notable changes of Iris 3.4 are as follows:
* Coq 8.13 is now supported; the old Coq 8.9 and Coq 8.10 are not supported any
more.
* The new `view` RA construction generalizes `auth` to user-defined abstraction
relations. (thanks to Gregory Malecha for the inspiration)
* The new `dfrac` RA extends `frac` (fractions `0 < q ≤ 1`) with support for
"discarding" some part of the fraction in exchange for a persistent witness that
discarding has happened. This can be used to easily generalize fractional
permissions with support for persistently owning "any part" of the resource. (by
Simon Friis Vindum)
* The new `gmap_view` RA provides convenient lemmas for ghost ownership of
heap-like structures with an "authoritative" view. Thanks to `dfrac`, it
supports both exclusive (mutable) and persistent (immutable) ownership of
individual map elements.
* With this release we are beginning to provide logic-level abstractions for
ghost state, which have the advantage that the user does not have to directly
interact with RAs to use them.
- `ghost_var` provides a logic-level abstraction of ghost variables: a
mutable "variable" with fractional ownership.
- `mono_nat` provides a "monotone counter" with a persistent witnesses
representing a lower bound of the current counter value. (by Tej Chajed)
- `gset_bij` provides a monotonically growing partial bijection; this is
useful in particular when building binary logical relations for languages with a
heap.
* HeapLang provides a persistent read-only points-to assertion `l ↦□ v`. (by
Simon Friis Vindum)
* We split Iris into multiple opam packages: `coq-iris` no longer contains
HeapLang, which is now in a separate package `coq-iris-heap-lang`. The two
packages `coq-iris-deprecated` (for old modules that we eventually plan to
remove entirely) and `coq-iris-staging` (for new modules that are not yet ready
for prime time) exist only as development versions, so they are not part of this
release.
* The proofmode now does a better job at picking reasonable names when moving
variables into the Coq context without a name being explicitly given by the
user. However, the exact variable names remain unspecified. (by Tej Chajed)
Further details are given in the changelog at
<https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md>.
This release of Iris was managed by Ralf Jung and Robbert Krebbers, with
contributions by Arthur Azevedo de Amorim, Dan Frumin, Enrico Tassi, Hai Dang,
Michael Sammler, Paolo G. Giarrusso, Rodolphe Lepigre, Simon Friis Vindum, Tej
Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
For std++, Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no
longer supported.
This release of std++ was managed by Ralf Jung and Robbert Krebbers, with
contributions by Alix Trieu, Dan Frumin, Hugo Herbelin, Paulo Emílio de Vilhena,
Simon Friis Vindum, and Tej Chajed. Thanks a lot to everyone involved!
For further details, see the full changelog at
<https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md>.
Both packages are available in the Coq opam registry. For further information
and installation instructions for Iris and std++, see the respective project
websites:
* https://gitlab.mpi-sws.org/iris/iris
* https://gitlab.mpi-sws.org/iris/stdpp
If you have any questions, feel free to reply to this email, or join our
community chat room <https://iris-project.org/chat.html>.
Best,
The Iris and std++ teams
More information about the Iris-Club
mailing list