Explore projects

opam repository for development versions of things we develop.

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

The Coq development of LambdaRust

Local Simulation proofs, the Iris style

A logic for proving contextual refinements [project website]

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

The Coq development for Iris

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

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

Automation for Iris

The main Coq development.

Some example verification demonstrating the use of Iris.

An extended "Standard Library" for Coq

Our pile of linear algebra

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