coq-iris

Iris is a Higher-Order Concurrent Separation Logic for reasoning about fine-grained concurrent programs, building logical relations, and more. It features an interactive proof mode for carrying out separation logic proofs in Coq.

opam install coq-iris.3.0.0
homepage
http://iris-project.org/
license
BSD
bugs tracker
https://gitlab.mpi-sws.org/FP/iris-coq/issues
dependencies
coq (((>= 8.5.1 & < 8.7~) | (= dev))) & coq-mathcomp-ssreflect (((>= 1.6.1 & < 1.7~) | (= dev)))
source
https://gitlab.mpi-sws.org/FP/iris-coq/repository/archive.tar.gz?ref=iris-3.0.0
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-iris/coq-iris.3.0.0