Explore projects

The main Coq development.

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

Coq development for the Semantics course taught at Saarland University

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

Local Simulation proofs, the Iris style

opam repository for development versions of things we develop.

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

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

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

A logic for proving contextual refinements [project website]

Automation for Iris

golang implementation of X-Trace and pubsub, also including some funky rewriting in order to get goroutine local variables.

Currently, the golang imports still point back to the repository hosted on GitHub. Depends on the tracingplane-go repository.

This project contains some scripts and other files that are used by many Iris project for their CI

The Coq development for Iris

The Coq development of LambdaRust

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

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