The Coq development for Iris. [project website] [coqdoc]
An extended "Standard Library" for Coq. [coqdoc]
The Coq development of LambdaRust
opam repository for development versions of things we develop.
The main Coq development of the Prosa project: http://prosa.mpi-sws.org
Axiomatic pWCET, formalized in Coq
Safety of a syntactically unsafe symbol ADT.
Deprecated repository; please use the POPL 2021 version instead
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
The Iron logic for precise reasoning about resources [project website]
Prototype DNN Serving System that can support thousands of models, dozens of worker machines, and low-latency SLOs. (OSDI '20)