Explore projects

A logic for proving contextual refinements project website(https://cs.ru.nl/~dfrumin/reloc/)

The Coq development of LambdaRust

The Coq development of LambdaRust

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

Some example verification demonstrating the use of Iris.

Logically Atomic Triples in Iris

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

Unmaintained repository. An extension of the Iris program logic to support linearity and fair refinement reasoning.

The Coq development of LambdaRust

Some example verification demonstrating the use of Iris.

The main Coq development.

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

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

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

The Coq development of LambdaRust

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

The Iron logic for precise reasoning about resources project website(https://iris-project.org/iron/)

The Iron logic for precise reasoning about resources project website(https://iris-project.org/iron/)

This is a demo showing how the the Iris Proof Mode can be used with FSCQ.