Explore projects

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

A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.

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

The Coq development of LambdaRust

The Coq development for Iris

Logically Atomic Triples in Iris

The Coq development for Iris

The main Coq development.

The Coq development for Iris

The main Coq development.

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

OLD VERSION, SEE https://gitlab.mpi-sws.org/iris/reloc INSTEAD

Logically Atomic Triples in Iris

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