Explore projects

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

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

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

The Coq development of LambdaRust

opam repository for development versions of things we develop.

Some example verification demonstrating the use of Iris.

An extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/)

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

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

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

A logic for proving contextual refinements project website(https://cs.ru.nl/~dfrumin/reloc/)

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