Dear Coq users,
We are pleased to announce the release of Iris 3.2 and std++ 1.2.1.
The highlight of the new Iris release is the completely re-engineered interactive proof mode. Not only did many tactics become more powerful; the entire proof mode can now be used not just for Iris but also for other separation logics satisfying the proof mode interface (e.g., Iron and GPFSL). Also see the accompanying paper.
Beyond that, the Iris program logic gained the ability to reason about potentially stuck programs, and a significantly strengthened adequacy theorem that unifies the three previously separately presented theorems. There are now also Hoare triples for total program correctness (but with very limited support for invariants) and logical atomicity.
And finally, our example language HeapLang was made more realistic (Compare-and-set got replaced by compare-exchange and limited to only compare values that can actually be compared atomically) and more powerful, with added support for arrays and prophecy variables.
The std++ release is mostly a patch release, and contains no major changes. The full list of changes is documented in the Iris changelog and std++ changelog, respectively.
Iris 3.2 and std++ 1.2.1 should appear in Coq’s opam repository soon. If you have any questions, don’t hesitate to contact us on our mailing list, or join the Iris chat room. We also welcome bug reports and pull requests at the Iris and std++ GitLab projects.
For examples showing how to use Iris, have a look at the Iris case studies we maintain in the examples repository. We will make sure they are always compatible with the latest version of Iris. Lecture material for Iris is available on our website. For further information, visit the Iris project page.
These releases of Iris and std++ received contributions from Aleš Bizjak, Amin Timany, Dan Frumin, Glen Mével, Hai Dang, Hugo Herbelin, Jacques-Henri Jourdan, Jan Menz, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Joseph Tassarotti, Mackie Loeffel, Marianna Rapoport, Maxime Dénès, Michael Sammler, Paolo G. Giarrusso, Paulo Emílio de Vilhena, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Simon Spies, and Tej Chajed. Thanks a lot to everyone involved!
Best,
The Iris and std++ team