Explore projects

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

opam repository for development versions of things we develop.

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

A tutorial for the Iris Separation Logic Framework

Coq development for the Semantics course taught at Saarland University

Iris with transfinite step-indexing

Deprecated project. An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode

Some example verification demonstrating the use of Iris.

The main Coq development of the NCCoq project