[Iris-Club] Iris 4.2 and std++ 1.10
Ralf Jung
research at ralfj.de
Fri Apr 12 15:21:12 CEST 2024
Hi everyone,
We are happy to announce the release of Iris 4.2 and std++ 1.10. 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 of this new Iris version are:
* We have new laws to "undiscard" discarded fractions, allowing one to update
from `DfracDiscarded` to `DfracOwn(q)` for some fresh `q`. This gives rise to
new laws for all constructions that use `dfrac`, such as
`ghost_map_elem_unpersist : ∀ k γ v, k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{#q} v`.
* The `gmap_view K V` camera now supports value types `V` that are arbitrary
cameras, and lifts their composition to the whole map. The previous `gmap_view`
type can be recovered as `gmap_view K (agree V)`.
* The `iFrame` tactic has become stronger for goals that contain existential
quantifiers: `iFrame` will now attempt to instantiate these. For example,
framing `P x` in goal `Q ∗ ∃ y, P y ∗ R` will now succeed with remaining goal `Q
∗ R`.
For std++, the biggest new feature in this release is the bitvector library with
support for fixed-size integers. It is distributed as a separate package,
`coq-stdpp-bitvector`. The library is developed and maintained by Michael
Sammler.
The supported Coq versions are 8.18 and 8.19.
For further details, see the full changelog of Iris at
https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-420-2024-04-12
and std++ at
https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-1100-2024-04-12.
This release was managed by Ralf Jung and Robbert Krebbers.
std++ received further contributions from Mathias Adam Møller, Michael Sammler,
Pierre Rousselin, Pierre Roux, and Thibaut Pérami.
Iris received further contributions from Ike Mulder, Jan-Oliver Kaiser, Johannes
Hostert, Pierre Roux, Thomas Somers, and Yixuan Chen.
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:
* 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 Iris
community chat room: https://iris-project.org/chat.html.
Best,
The Iris and std++ teams
More information about the Iris-Club
mailing list