The Coq development for Iris. [project website] [coqdoc]
An extended "Standard Library" for Coq. [coqdoc]
Axiomatic pWCET, formalized in Coq
The Coq development of LambdaRust
The main Coq development of the Prosa project: http://prosa.mpi-sws.org
Iris with transfinite step-indexing
Deprecated project. An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode
Prototype DNN Serving System that can support thousands of models, dozens of worker machines, and low-latency SLOs. (OSDI '20)
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)