The Coq mailing list

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

Dear Coq-Clubbers,

We are happy to announce the release of *Iris 3.1*.  Iris is a higher-order
concurrent separation logic and a Coq framework for performing interactive
program verification using said logic.  You can find more information at
<http://iris-project.org/>.  This is the Iris release that will be used at the
upcoming Iris tutorial at POPL'18.

For examples showing how to use Iris, have a look at the Iris case studies we
maintain at <https://gitlab.mpi-sws.org/FP/iris-examples>.  We will make sure
they are always compatible with the latest version of Iris.  Lecture material
for Iris is available at <http://iris-project.org/tutorial-material.html>.

This release includes many improvements and extensions, both to the theory of
Iris, its derived constructions, and the Coq infrastructure.  On the Coq side,
we mostly worked on making the interactive proof mode more consistent and more
expressive, accounting for the needs of the growing number of projects that 
rely
on it.  The full list of changes is documented in our Changelog at
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/CHANGELOG.md>.

Iris 3.1 should appear in Coq's opam repository soon.  If you have any
questions, don't hesitate to contact us on our mailing list at
<https://lists.mpi-sws.org/listinfo/iris-club>, or join the recently created
Iris chat room at <https://mattermost.mpi-sws.org/iris>.  We also welcome bug
reports and pull requests at <https://gitlab.mpi-sws.org/FP/iris-coq/>.

Next to Iris 3.1, we are happy to release std++ 1.1: an "extended standard
library" for Coq, which provides many definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets, as
well as tactics and other infrastructure for reasoning about these. This 
library
used to be part of Iris, but has become a separate project since this Iris
release.  More information is available on the project website at
<https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/>.

Both Iris 3.1 and std++ 1.1 are compatible with Coq 8.6.1 and newer.

On behalf of the Iris team,
Ralf