The Coq mailing list

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

Hi Ralf,

Thanks for your reply. Do you want to bite the bullet ;) SwissPost [1] has a substantial codebase written in Java.

Best,

Mukesh

[1] https://gitlab.com/swisspost-evoting/crypto-primitives/crypto-primitives

On Thu, Oct 12, 2023 at 5:18 PM Ralf Jung <research AT ralfj.de> wrote:

Hi Mukesh,

There exist Iris formalizations of (subsets of) at least Rust, Go, OCaml and
WebAssembly, and an axiomatization of C++. There is a Scala type soundness proof
in Iris but I don't think it comes with a separation logic that can be used to
reason about imperative Scala. I'm not familiar with any work specifically on
Java, unfortunately.

Kind regards,
Ralf

On 12.10.23 15:00, mukesh tiwari wrote:
> 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
> <mailto: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/
>     <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
>     <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/ <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
>     <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 <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 <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 contributionsfrom 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/iris>
>     * https://gitlab.mpi-sws.org/iris/stdpp <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
>     <https://iris-project.org/chat.html>).
>
>     Best,
>     The Iris and std++ teams
>

--
Website: https://research.ralfj.de