The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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), 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