Hi everyone,
We are happy to announce the release of Iris 4.3 and std++ 1.11. 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.
This Iris release mostly features quality-of-life improvements, such as improvements to iInduction, a new iUnfold tactic, and improved errors in iInv. For std++, the biggest new feature in this release provides stronger versions of the induction principles for map_fold, exposing the order in which elements are processed. Both releases of Iris and std++ now support dune compilation.
For Iris, the supported Coq versions are 8.19 and 8.20, while std++ also supports Coq 8.18.
For further details, see the full changelog of Iris at CHANGELOG.md · master · Iris / Iris · GitLab and std++ at CHANGELOG.md · master · Iris / stdpp · GitLab.
This release was managed by Jesper Bengtson, Ralf Jung and Robbert Krebbers.
std++ received contributions from Andres Erbsen, Lennard Gäher, Léo Stefanesco, Marijn van Wezel, Paolo G. Giarrusso, Pierre Roux, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Yannick Zakowski, and Yiyun Liu.
Iris received contributions from Benjamin Peters, Isaac van Bakel, Jan-Oliver Kaiser, Janggun Lee, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Tej Chajed, William Mansky, and Yusuke Matsushita.
Thanks a lot to everyone involved!
Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:
If you have any questions, feel free to reply to this email, or join our Iris community chat room: Iris Chat Room: Iris Chat Room.
Best,
The Iris and std++ teams