Open Source Projects

Here is a short inventory of my various open-source projects, both big and small. Most of these projects also come with a dedicated web page, which you can achieve by clicking on the highlighted project name. If you would like to contribute any code, bug reports, improvements or random thoughts, feel free to contact me.

Current Projects

FunCC, a formally-verified, verifying and standards-compliant C compiler suite. This is currently my main hobby project, in which I attempt to continue the work begun during my PhD research, aiming to implement a complete C compiler that is subject to stringent and formally-verified correctness guarantees, complies with the precise ANSI C89 and C99 standard specifications of the language, supports all known GNU C extensions, performs extensive optimisations of the generated programs and, last but not least, accomodates and aids formal reasoning about arbirary correctness properties of the actual C programs being compiled, effectively answering Tony Hoare's grand challenge for computer science. Easy as a pie, eh? Well, these are the aims of the project, the actual expectations are somewhat more modest and, in reality, I intend FunCC to represent simply a bagful of pragmatic results from my research in the area of program translation. For the current status and progress, please check out the FunCC project page.
lambdaT_EX, a sophisticated typesetting system for Haskell (and other) source code, written entirely in T_EX and, accordingly, requiring no preprocessor or other external tools. Originally conceived as a silly experiment in T_EX hacking, the system has since been applied in a number of serious projects, including my own PhD dissertation.
libunidata, an attempt to capture the entirety of information contained in the Unicode Character Database. While there are other similar libraries around, libunidata is the only one that is designed for portability and sharing across programming languages, currently providing bindings for C, C++ and Haskell.

Miscellaneous Endeavours

Interesting and potentially useful code that doesn't really qualify as a full-featured project. Still, I welcome your comments, improvements and suggestions regarding these little nibbles.

Models of LCF, my reprint of Robin Milner's seminal 1973 paper by the same title. The original technical report, available from Stanford University, was badly corruped by a non-discriminative attempt to apply a dubious optical character recognision to Milner's hand-written formulae, rendering much of the material all but illegible. As my own little personal tribute to one of the greatest computer scientists of our time, I have rendered the report in T_EX, taking every care to preserve the original content as much as possible within the constraints imposed by the poor quality of its publically-available digitised version.
TenDRA, original sources of the amazing TenDRA C/C++ compiler suite, which I'm hosting here for archival purposes on the request of one of their authors, Dr. Phil Core.
K-Fish Generator, a small ASCII art generator written entirely in T_EX. If you must be serious, take it as a proof of concept; otherwise, just enjoy a little K-fish in your life!

Past Projects

The following projects are now deemed dormant and of historical interest only. I include them here in case someone finds some of my code useful, but please do not expect me to fix any bugs or provide help with the installation and usage of this material.

Sulima, an extendible instruction set simulator framework, including a design of an algorithm for a speculative, distributed, lock-free and cycle-accurate instruction simulation inspired by the IVY distributed shared memory algorithm described in Kai Li and Paul Hudak in Memory Coherence in Shared Virtual Memory Systems, ACM Transactions on Computer Systems, Vol. 7(4), November 1989. A partial implementation of Sulima constituted my undergraduate honours thesis.