Explore projects
-
-
The Coq development for Iris. [project website] [coqdoc]
Updated -
Coq development for the Semantics course taught at Saarland University
Updated -
Updated
-
Prototype DNN Serving System that can support thousands of models, dozens of worker machines, and low-latency SLOs. (OSDI '20)
Updated -
Local Simulation proofs, the Iris style
Updated -
-
The Coq development for Iris. [project website] [coqdoc]
Updated -
Updated
-
An extended "Standard Library" for Coq. [coqdoc]
Updated -
The main Coq development of the Prosa project: http://prosa.mpi-sws.org
Updated -
A logic for proving contextual refinements [project website]
Updated -
Updated
-
-
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.
Updated -
-
The Coq development for Iris
Updated -
The Coq development of LambdaRust
Updated -
A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)
Updated -
The Iron logic for precise reasoning about resources [project website]
Updated