coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Iris release 3.0

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Iris release 3.0
Date: Thu, 12 Jan 2017 16:45:52 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:c9yP5BVDOnnWoiVZJgmBPsxfATzV8LGtZVwlr6E/grcLSJyIuqrYZROPt8tkgFKBZ4jH8fUM07OQ6PG8HzdYqsbZ+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/4cnppMaWO1kAxGflIOA6EBLjpgLI88ISnIFKK6AryxKPrGEbVf5RwDZSLFad1zTh4Mj4qJx+9St4vuogstVfSuP9ZatuHu8QNygvL21gvJ6jjhLEVwbauyMR

Hi all,

we are happy to announce the release of the Coq development for Iris
3.0. Iris is a higher-order concurrent separation Logic for reasoning
about fine-grained concurrent programs, building logical relations, and
more. The Coq development features an interactive proof mode for
conveniently carrying out separation logic proofs in Coq.

The Iris Coq development is available in Coq's opam repository as
coq-iris. It is compatible with Coq 8.5pl3 and 8.6, and furthermore
requires ssreflect 1.6.1. Fur further information, visit our website at
<http://iris-project.org/> or check out the source repository at
<https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0>. Many of us will
be at POPL, so that's also a great opportunity to get questions answered :)

Kind regards,
Ralf

[Coq-Club] Iris release 3.0, Ralf Jung, 01/12/2017