Explore projects

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

The Coq development of LambdaRust

The main Coq development.

The Coq development for Iris

The main Coq development.

The Coq development for Iris

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

The main Coq development.

Logically Atomic Triples in Iris

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

opam repository for development versions of things we develop.

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

Some example verification demonstrating the use of Iris.

The main Coq development.

The main Coq development.

Safety of a syntactically unsafe symbol ADT.