Explore projects

Some example verification demonstrating the use of Iris.

Safety of a syntactically unsafe symbol ADT.

Deprecated repository; please use the POPL 2021 version instead

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

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

Automation for Iris

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

A logic for proving contextual refinements [project website]

The Coq development of LambdaRust

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

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

Logically Atomic Triples in Iris

An extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/)

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

Unmaintained repository. See here for a maintained fork.

Formalizes the ordered RA model of Iris from the MoSeL paper

Coq development for "The High-Level Benefits of Low-Level Sandboxing"

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

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