Explore projects

Operational Repaired C11

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

This repo contains our prototype implementing the generalised projection of global types from our MST framework with generalised choice.

Maintainer: Felix Stutz

The Coq development of LambdaRust

rLTL to LTL rewriter

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

Some example verification demonstrating the use of Iris.

Public repository of the paper 'Constraint Synthesis for Parametric CAD'.

A certificate checker for roundoff error bounds

Mirror of https://github.com/dmlc/tvm for internal development

Check other branches for active development.

Don't forgot to git submodule init and git submodule update!

A logic for proving contextual refinements project website(https://cs.ru.nl/~dfrumin/reloc/)

Local Simulation proofs, the Iris style

opam repository for old versions of things we develop (to avoid accumulating too many versions in the main repository)

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.