The Coq development for Iris. [project website] [coqdoc]
An extended "Standard Library" for Coq. [coqdoc]
The Coq development of LambdaRust
The main Coq development of the Prosa project: http://prosa.mpi-sws.org
A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.
OLD VERSION, SEE https://gitlab.mpi-sws.org/iris/reloc INSTEAD
Safety of a syntactically unsafe symbol ADT.
Deprecated repository; please use the POPL 2021 version instead
The Iron logic for precise reasoning about resources [project website]
A tutorial for the Iris Separation Logic Framework
A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)
Some example verification demonstrating the use of Iris.
A logic for proving contextual refinements [project website]
Iris with transfinite step-indexing
Deprecated project. An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode
Coq development for the Semantics course taught at Saarland University
Local Simulation proofs, the Iris style