Software

by

This is a partial list of open-source software projects for which I am the primary contributor. My interests have been in reliability, scalability, distributed systems, compilers, and programming languages. Dates are approximate. Lines of code (loc) are raw, including comments.

1995-present. The MetaPRL theorem prover. A logical framework for reasoning about large software systems. 365K loc (OCaml, Computational Type Theory).

2003-present. The OMake build system. A build system, language, and shell for large software projects. The specification language is pure, ensuring compositionality. 233K loc (OCaml, C).

2002. The MCC compiler collection. An x86 compiler for C, Java, Caml; supporting speculations (transactions) and process migration. 351K loc (OCaml, C, x86).

2004-2008. The Mojavecomm scalable infrastructure for scalable globally, totally ordered group communication. (Research group project). 103K loc (OCaml, C).

2006-2008. The Mojave filesystem, a scalable, global distributed filesystem with Unix semantics. (Incomplete). 15K loc (OCaml, C).

2003. The MP compiler. A x86 compiler for an ML source language, written in type theory. 44K loc (Computational Type Theory).

2005. The libtrans group communication library, for highly scalable, globally consistent communication. But wait, there’s more — includes a CIFS server! 30K loc (OCaml, C).

2003. UserVFS. A device driver that implements a user-space filesystem API for Linux. 17K loc (C, OCaml).

2000. The Ambient compiler. An x86 compiler for the Ambient Calculus. 38K loc (OCaml).

1995. The Ensemble Jukebox. A peer-to-peer music sharing service using reliable group communication. 100K loc (OCaml, C).

1989. A C++ interpreter. It covers the language for 1989, except for templates. 19K loc (C++).

1988. The Jail-OS, a kernel for the Zilog Z8000 16-bit processor. 90K loc (Z8000 assembly). Unfortunately, this code is on tape, and I don’t have a tape drive…

1987. The Jail object-oriented language (a Lisp dialect), where everything is an object. 15K loc (C).

1983. A Z8000 assembler and interpreter (this code is a fragment). Zilog Inc. 15K loc (C).