Forked from
Iris / Iris
2416 commits behind the upstream repository.
README.md 6.66 KiB
IRIS COQ DEVELOPMENT coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)
This is the Coq development of the Iris Project, which includes MoSeL, a general proof mode for carrying out separation logic proofs in Coq.
For using the Coq library, check out the API documentation.
For understanding the theory of Iris, a LaTeX version of the core logic definitions and some derived forms is available in tex/iris.tex. A compiled PDF version of this document is available online.
Building Iris
Prerequisites
This version is known to compile with:
- Coq 8.9.1 / 8.10.2 / 8.11.2
- A development version of std++
If you need to work with Coq 8.7 or Coq 8.8, please check out the iris-3.2 branch.