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

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

A custom Akka dispatcher that logs and controls the delivery order of actor messages.

Daisy - a framework for accuracy analysis and synthesis of numerical programs

A calculus of logical relations for concurrency, formalized in Iris.

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

Safety of a syntactically unsafe symbol ADT.

The main Coq development.

opam repository for development versions of things we develop.

The main Coq development.

The Coq development for Iris

Logically Atomic Triples in Iris

The Coq development for Iris

Code for RedQueen paper for simulating user walls synthetically as well as using real data.

GITLab repository for privacy_capsules. This repository is for external read-only purposes. For development/contribution, please contact us to have access to MPI-SWS internal GIT.

The main Coq development.