[Iris-Club] [Coq-Club] Iris 4.1 and std++ 1.9 released

[mukesh tiwari]

Hi Johannes,

I have never used Iris so this question may not be wellformed. According to
my understanding of Iris, it can be used to reason about Rust programs but
my question is: is there anyone who has developed a framework in Iris to
reason about Java programs?

Best,
Mukesh


On Thu, 12 Oct 2023 at 09:25, Johannes Hostert <
s8johost at stud.uni-saarland.de> wrote:

> Hello everyone,
>
> We are happy to announce the **release of Iris 4.1 and std++ 1.9**. 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
> smarter handling of `->`/`<-` patterns by `iDestruct`, support for an
> arbitrary number of Coq intro patterns in the Iris proofmode tactics
> (`iIntros`, `iDestruct`, etc.), and support for immediately introducing the
> postcondition of a WP specification via `wp_apply lemma as "Hpost"`.
>
> The biggest changes and new features are:
> * Logically atomic triples now support private (non-atomic)
> postconditions, and the notation was changed to not clash with Autosubst
> any more. Existing users of logically atomic specifications have to update
> their notation, see the full  CHANGELOG for more details.
> * The meaning of `P -∗ Q` as a Coq proposition has changed from `P ⊢ Q` to
> `⊢ P -∗ Q`. If you are only using the Iris proofmode, this will not make a
> difference, but when writing proof scripts or tactics that `rewrite` or
> `apply` Iris lemmas, the exact position of the `⊢ P -∗ Q` matters and this
> will now always be visible in lemma statements.
> * `iCombine` is starting to gain support for a `gives` clause, which
> yields persistent facts gained from combining the resources. So far, this
> remains mostly experimental. We support `↦` and the connectives of ghost
> theories in `base_logic/lib`, but support for `own` and custom cameras is
> minimal and will be improved in future releases.
> * Some initial refactoring prepares Iris for eventually supporting
> transfinite step-indexing.
> * New resources algebras have been added: `Z`, `max_Z`, `mono_Z`, and
> `mra` (the monotone resource algebra of
> https://iris-project.org/pdfs/2021-CPP-monotone-final.pdf)
>
> For std++, the highlights of this release are:
> * `gmap` and related types are re-implemented based on Appel and Leroy's
> [Efficient Extensional Binary Tries](
> *https://inria.hal.science/hal-03372247*
> <https://inria.hal.science/hal-03372247>), making them usable in nested
> inductive definitions and improving extensionality. More information can be
> found in Robbert Krebbers' Coq Workshop talk, see
> https://coq-workshop.gitlab.io/2023/
> * New tactics `ospecialize`, `odestruct`, `oinversion` etc are added.
> These tactics improve upon `efeed` / `edestruct` by allowing one to leave
> more terms open when specializing arguments. For instance, `odestruct (H _
> x)` will turn the `_` into an evar rather than trying to infer it
> immediately, making it usable in many situations where `edestruct` fails.
> This can significantly shorten the overhead involved in forward reasoning
> proofs. For more information, see the test cases provided here:
> https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/tests/tactics.v#L114
>
> For further details, see the full changelog of Iris at
> https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-410-2023-10-11
> and std++ at
> https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-190-2023-10-11
>
> Iris 4.1 and std++ 1.9 support Coq 8.16-8.18.
>
> This release of Iris and std++ was managed by Ralf Jung, Robbert Krebbers,
> and Johannes Hostert.
>
> This Iris release received contributions from Amin Timany, Arthur Azevedo
> de Amorim, Armaël Guéneau, Benjamin Peters, Dan Frumin, Dorian Lesbre, Ike
> Mulder, Isaac van Bakel, Jaemin Choi, Janine Lohse, Jan-Oliver Kaiser,
> Jonas Kastberg Hinrichsen, Lennard Gäher, Mathias Adam Møller, Michael
> Sammler, Paolo Giarrusso, Pierre Roux, Rodolphe Lepigre, Simcha van Collem,
> Simon Friis Vindum, Simon Spies, Tej Chajed, Yicuan Chen, and Yusuke
> Matsushita.
>
> This std++ release received contributions from Dorian Lesbre, Herman
> Bergwerf, Ike Mulder, Isaak van Bakel, Jan-Oliver Kaiser, Jonas Kastberg,
> Marijn van Wezel, Michael Sammler, Paolo Giarrusso, Tej Chajed, and Thibaut
> Pérami.
>
> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20231012/cabf54ea/attachment-0001.html>