Explore projects

An extended "Standard Library" for Coq. [coqdoc]

The Coq development for Iris. [project website] [coqdoc]

The Coq development of LambdaRust

https://os.mpi-sws.org/

Axiomatic pWCET, formalized in Coq

opam repository for development versions of things we develop.

The main Coq development of the Prosa project: http://prosa.mpi-sws.org

A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)

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

The Iron logic for precise reasoning about resources [project website]