Explore projects

UniTraX is a data analytics system that provides users with a personal differentially private bound on privacy loss. UniTraX is able to allow more queries than previous systems, without giving up on analytic accuracy.

UniTraX data for experiments. See main repository at https://gitlab.mpi-sws.org/anon/unitrax for more information.

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

Some example verification demonstrating the use of Iris.

Exercises for the Iris tutorial

A fork of the Haskell Cabal repository that includes a change necessary for running the Class Struggle analysis, as part of Scott Kilpatrick's PhD thesis.

Generative Models are being developed currently which can potentially be used for various applications such as data generation for training models. This project aims to analyse a generative model, the Variational Autoencoder and potential bias in it.

Coq development for "The High-Level Benefits of Low-Level Sandboxing"

Unmaintained repository. An extension of the Iris program logic to support linearity and fair refinement reasoning.

A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.

A fork from in order to explore using (a subset of) LTL as a core language of Flipper

The Coq development of LambdaRust

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

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

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

The Coq development of LambdaRust