David Pearce

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

FeatherweightRust. Provides a reference implementation of FeatherweightRust in Java.

StronglyConnectedComponents. An example implementation of my algorithm for finding Strongly Connected Components.

jx86. Java Library for Generating x86 Code

jkit. Java Compiler Kit (JKit)

LeanEVM. A toy implementation of the EVM in Lean4.

JavaAVR. Simple AVR simulator written in Java

SyntacticHeap.rs. A generic data structure designed for representing Abstract Syntax Trees.

TuttePolynomial. Tutte Polynomial Computation

JModelGen. A model generator library for use with automated test generation.

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

EvmTools. Various utilities for working with the Etherem Reference Tests.

VirtualMachineInterpreter.rs. A utility for helping in the construction of interpreters / virtual machines.

Web.wy. A functional framework for creating single-page applications to execute in the browser.

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

TinyBoy. A simple AVR Games Console which resembles the Arduaboy, but is designed around the ATtiny85!

VcGen. A simple library for manipulating and generating verification conditions.

JSMT. A bunch of utilities / algorithms for implementing SMT solvers

JWebKit. A simple web framework, currently written in Java (though will eventually be in Whiley)

Minesweeper.wy. Implementation of Minesweeper in Whiley

Pacman. A Multi-Player Implementation of Pacman in Java

WyrlVis. A Visualation Tool for the Whiley Rewrite Language. This allows automata and rewrites to be visualised, which is helpful for debugging (amongst other things).

TokenContract.wy. A simple smart contract written in Whiley.

BettingContract. A simple betting smart contract written in Solidity.

JSyntacticHeap. A simple Java library for reading / writing files according to the SyntacticHeap format.

WhileyComparison. A repository of small programs to be implemented and verified by Whiley and various other verification and static analysis tools

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

Lil.rs. A low-level intermediate language written Rust.

DevmProofGen. Dafny Evm Proof Generator (experimental)

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

WebCalc.wy. A simple calculator implemented as a Single Page App in Whiley.

Homepage. My personal homepage.

JBuildGraph. A library for managing builds (e.g. within a compiler).