We are happy to announce the release of Iris 3.6 and std++ 1.7. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.
The highlights and most notable changes of Iris 3.6 are:
- Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.
Coq 8.12 is no longer supported.
- Support for discardable fractions (
dfrac) has been added to
authoritative elements, and to the
mono_natlibrary. See below for other
- A new
mono_listalgebra provides monotonically growing lists with an
exclusive authoritative element and persistent prefix witnesses. See
iris/algebra/lib/mono_list.vfor details. An experimental logic-level
library wrapping the algebra is available at
iris_staging/base_logic/mono_list.v; if you use it, please give feedback on
the tracking issue
Further details are given in the changelog at CHANGELOG.md · master · Iris / Iris · GitLab
This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with
contributions from Dan Frumin, Jonas Kastberg Hinrichsen, Lennard Gäher,
Matthieu Sozeau, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert
Krebbers, Simon Friis Vindum, Tej Chajed, and Vincent Siles. Thanks a lot to
For std++, Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain supported. Coq 8.10 is no longer supported.
This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a lot to everyone involved!
For further details, see the full changelog at CHANGELOG.md · master · Iris / stdpp · GitLab
Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites: