Explore projects

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]

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

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

The Coq development of LambdaRust

Instrumented fork of Apache Kafka from GitHub

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