Explore projects

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

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

The Coq development of LambdaRust

opam repository for development versions of things we develop.

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

Axiomatic pWCET, formalized in Coq

Safety of a syntactically unsafe symbol ADT.

Deprecated repository; please use the POPL 2021 version instead

A tutorial for the Iris Separation Logic Framework

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

Some example verification demonstrating the use of Iris.

A logic for proving contextual refinements [project website]

Iris with transfinite step-indexing

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

Coq development for the Semantics course taught at Saarland University

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

Prototype DNN Serving System that can support thousands of models, dozens of worker machines, and low-latency SLOs. (OSDI '20)