The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi everyone,

We are happy to announce the release of Iris 4.0 and std++ 1.8. 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 highlight of Iris 4.0 is the *later credits* mechanism, which provides a 
new
way to eliminate later modalities.

This new mechanism complements the existing techniques of taking program 
steps,
exploiting timelessness, and various modality commuting rules. At each program
step, one obtains a credit `£ 1`, which is an ownable Iris resource. These
credits don't have to be used at the present step, but can be saved up, and 
used
to eliminate laters at any point in the verification using the fancy update
modality. Later credits are particularly useful in proofs where there is not a
one-to-one correspondence between program steps and later eliminations, for
example, logical atomicity proofs. As a consequence, we have been able to
simplify the definition of logical atomicity by removing the 'laterable'
mechanism.

The later credit mechanism is described in detail in the
[ICFP'22 paper](https://plv.mpi-sws.org/later-credits/) and there is a
[small 
tutorial](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/tests/later_credits_paper.v)
in the Iris repository. The
[examples](https://gitlab.mpi-sws.org/iris/examples/) repository contains some
logically atomic case studies that make use of later credits: the counter 
with a
backup (Section 4 of the later credits paper), as well as the elimination 
stack,
conditional increment, and RDCSS.

Iris 4.0 supports Coq 8.13 - 8.16. For all the details, and a sed script that 
helps with porting code using Iris, see 
<https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-400-2022-08-18>.

This release was managed by Ralf Jung, Robbert Krebbers, and Lennard Gäher, 
with
contributions from Glen Mével, Gregory Malecha, Ike Mulder, Irene Yoon,
Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard Gäher, Michael Sammler,
Niklas Mück, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies,
and Tej Chajed. Thanks a lot to everyone involved!

For std++, Coq 8.16 is newly supported by this release, and Coq 8.12 to 8.15 
remain supported. Coq 8.11 is no longer supported. For more details, see 
<https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-180-2022-08-18>.

This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Lennard
Gäher, with contributions from Andrej Dudenhefner, Dan Frumin, Gregory 
Malecha,
Jan-Oliver Kaiser, Lennard Gäher, Léo Stefanesco, Michael Sammler, Paolo G. 
Giarrusso, Ralf Jung, Robbert Krebbers, and Vincent Siles. 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