Utilities for working with Polynomials

Dafny Evm Proof Generator (experimental)

Various utilities for working with the Etherem Reference Tests.

My personal homepage.

A toy implementation of the EVM in Lean4.

Parser library

A simple example illustrating the Z3 bindings for Rust. The purpose of this is to gain experience working directly with Z3.

C++ code accompanying the paper "A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs".

Tutte Polynomial Computation

Tools for checking the output of a Decomposed Tutte Computation

A simple betting smart contract written in Solidity.

A simple library for manipulating and generating verification conditions.

A generic data structure designed for representing Abstract Syntax Trees.

A simplistic viewer for Rank 1 Constraint Systems written in Rust.

Utilities for describing proof derivations.

A library for describing delta transformations and incremental computation.

An API written in Rust for parsing Whiley files and more!

A proof of the semantic subtyping relation from an academic paper.

A simple smart contract written in Whiley.

A library describing computation which can be divided into small steps.

A Cell-like structure for maintaining type-level invariants.

A library for parsing Whiley test files.

A demonstration of how Whiley can be used to verify compiler optimisations on a simple bytecode language.

A Rust port of the WhileyWeb system. This allows Whiley programs to be edited, compiled and executed from a single webpage.

A library providing implementations for unbound integers.

An HTML5 Canvas Implemetation of Conway's Game of Life written in Whiley

Implementation of Minesweeper in Whiley

Library for handling LZ77 and LZW compression and decompression.