Explore projects

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

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

The Coq development of LambdaRust

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

Safety of a syntactically unsafe symbol ADT.

Deprecated repository; please use the POPL 2021 version instead

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

A logic for proving contextual refinements [project website]

Some example verification demonstrating the use of Iris.

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

Iris with transfinite step-indexing

Local Simulation proofs, the Iris style

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