Explore projects

The main Coq development.

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

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

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

Our pile of linear algebra

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

opam repository for development versions of things we develop.

Local Simulation proofs, the Iris style

Automation for Iris

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

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

This repo contains our prototype implementing the generalised projection of global types from our MST framework with generalised choice.

Maintainer: Felix Stutz

The Coq development for Iris

Some example verification demonstrating the use of Iris.

This project contains some scripts and other files that are used by many Iris project for their CI

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

The Coq development of LambdaRust

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