(Major) Current Projects

As part of my PhD thesis I implemented:

  • A formalization of category theory in Coq.

  • A formalization of the Haskell compiler's intermediate language in Coq, including proofs that the various interestings structures (types+exprs, contexts+derivations, etc) form categories and the ability to extract Coq code which manipulates these formalized structures into Haskell code that can be linked in as a compiler pass.

  • The Haskell garrows library

  • The -XHetMet flag for GHC, which enables multi-level types and expressions.

  • The -fflatten flag for GHC, which performs a type-preserving flattening transformation from typed multi-level terms to typed expressions with an additional GArrow parameter. This pass is written in Coq as an operation on categories, using the formalization above, and the code for -fflatten is the Haskell extraction of the proof.

I'm currently working on WIX

I develop and use Ibex Mail

I wrote (and maintain) SBP, the Scannerless Boolean Parser

I'm working a bit on the Electric VLSI System from Static Free Software; here are my contributions.

I wrote Electric's BTree, which can be used independently of Electric.

Past Projects

I've written some software for hcoop. In particular, I wrote libnss-afs

I've contributed to OpenAFS.

I wrote space annealer.

I've written a Haskell implementation of the Terauchi+Aiken determinism algorithm; you can get the code here

I created slipway and abits

Brian Alliet and I wrote NestedVM

Way back in the day I wrote the first IMAP interface to GMail (before Google offered an official one). This was based on IbexMail (see above).

I created XWT, an open source platform for thin-client user interfaces. It's currently known as Ibex.

I wrote a fairly complete byte-compiled JavaScript interpreter in Java. Caveats: it doesn't implement JavaScript5 classes and does not distinguish between null and undefined.

I also wrote TinySSL, a lightweight SSL implementation in Java. Apparently somebody has turned it into an SSL provider

I did most of the work involved in implementing Win32 support for gcj, the Java frontend to gcc.

Minor Stuff

Some  performance data I collected regarding a GC-Ramdisk I bought. It's basically a bunch of DIMMs on a PCI card with a battery backup, pretending to be a SATA drive. The advantage over spinning disks, flash, or normal RAM is that this device has a lower latency-to-nonvolatile-state than anything else (flash has higher latency and non-battery-backed RAM is volatile). This (in theory) makes it ideal for a filesystem journal or ZFS intent log.

A simple script I wrote to make debian packages out of resin distributions.

I've written some Java code to control Zebra (formerly Eltron) 2684 Label Printers over a plain old RS-232 serial port. These printers are dirt cheap (I got mine for $25 each), incredibly high quality, and UPS gives away the labels (4“x6” adhesive) basically for free to their “WorldShip” customers, many of whom resell them for nearly nothing on eBay. It's an incredible deal. Here's a git repo with the code and manuals.

A registry patch to swap the control and capslock keys in Win2k and another registry patch to disable the left windows key (I didn't write this). Very useful with Parallels.


Random links: