David Pearce's Projects
Bindings for the ACE Editor (see https://ace.c9.io)
A collection of simple games for the Arduboy
An implementation for the classic arcade game "Asteroids" in Whiley
A simplified smart contract for holding auctions.
A demonstration which illustrates how Whiley can be used to verify compiler optimisations for the AVR instruction set.
A simple betting smart contract written in Solidity.
A library providing implementations for unbound integers.
A simple web application for implementing a blogging site. The purpose is to demonstrate and test the various features provided by JWebKit.
A Rust API for constructing and verifying Boogie programs.
Simple tool written in Rust for checking chess games.
A Cell-like structure for maintaining type-level invariants.
An HTML5 Canvas Implemetation of Conway's Game of Life written in Whiley
A library for describing delta transformations and incremental computation.
Utilities for describing proof derivations.
Dafny Evm Proof Generator (experimental)
C++ code accompanying the paper "A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs".
PCB schema and other files for my embedded projects.
Runtime Library for Ethereum Smart Contracts in Whiley
Various utilities for working with the Etherem Reference Tests.
Provides a reference implementation of FeatherweightRust in Java.
A small library for encoding / decoding GIFs.
A marking tool for git history.
My personal homepage.
An in-memory data representation with a functional API.
A Java emulator for the Arduboy 8-bit gaming platform (see arduboy.com) built around the JavaAVR emulator for AVR microcontrollers.
Simple AVR simulator written in Java
A serialisation scheme perhaps reminiscent of protobuf, where binary content can be transformed to/from Java Objects based on provided schema's. There are some differences though. In particular, binary content can be modifieA serialisation scheme perhaps reminiscent of protobuf, where binary content can be transformed to/from Java Objects based on provided schema's. There are some differences though. In particular, binary content can be modified (within the bounds of its schema) producing new content as a delta over the original.
A small library for manipulating immutable binary blobs.
A library for managing builds (e.g. within a compiler).
A compiler framework