Explore projects

opam repository for development versions of things we develop.

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

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

Local Simulation proofs, the Iris style

The main Coq development.

An extended "Standard Library" for Coq

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

Our pile of linear algebra

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

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]