Iris 3.3 and std++ 1.4

Announcements
1

Hello everyone,

We are pleased to announce the release of Iris 3.3, a concurrent separation logic framework for Coq. For an overview of the numerous research projects employing Iris, see https://iris-project.org/. Iris 3.3 is accompanied by std++ 1.4, an extended “standard” library for Coq.

This Iris release does not have any outstanding highlights, but contains a large number of improvements all over the board. For instance:

  • heap_lang (the default programming language shipped with Iris) now supports deallocation as well as better reasoning about “invariant locations” (locations that perpetually satisfy some Coq-level invariant).
  • Invariants (inv N P) are more flexible, now also supporting splitting and merging of invariants with respect to separating conjunction.
  • Performance of the proofmode for BIs (instances of the “Bunched Implication” algebra) constructed on top of other BIs (e.g., monPred) was greatly improved, leading to up to 70% speedup in individual files. As part of this refactoring, the proofmode can now also be instantiated with entirely “logical” notion of
    BIs that do not have a (non-trivial) metric structure, and still support reasoning about ▷.
  • The proof mode now provides experimental support for naming pure facts in intro patterns. See https://gitlab.mpi-sws.org/iris/string-ident for details.
  • Iris now provides official ASCII notation. We still recommend using the Unicode notation for better consistency and interoperability with other Iris libraries, but provide ASCII notation for when Unicode is not an option.
  • We removed several coercions, fixing “ambiguous coercion path” warnings and solving some readability issues.
  • Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and 8.8 are no longer supported.
    Further details are given in the full changelog at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md.

This release of Iris received contributions by Abel Nieto, Amin Timany, Dan Frumin, Derek Dreyer, Dmitry Khalanskiy, Gregory Malecha, Jacques-Henri Jourdan, Jonas Kastberg, Jules Jacobs, Matthieu Sozeau, Maxime Dénès, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Spies, and Tej Chajed.

For std++, Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported. For further details, see the changelog at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md. This release of std++ received contributions by Gregory Malecha, Michael Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, sarahzrf, and Tej Chajed.

Thanks a lot to everyone involved!

Both packages will be available in the Coq opam registry shortly. For further information and installation instructions for Iris and std++, see the respective project websites:

Best,
The Iris and std++ teams