These days my main project is the OCaml compiler. You can see my contributions to Jane Street's branch of the OCaml compiler here and here, or my contributions to upstream OCaml here.
Some open-source projects I worked on at Draper:
- VIBES is a patch compiler. It compiles source-level code fragments, edits them into existing binaries, and formally verifies that the resulting binary has only the intended changes.
- CBAT is a collection of binary analysis tools built on CMU's Binary Analysis Platform (BAP). CBAT includes an SMT-based weakest precondition analysis for BAP and various features for using it to analyze a single program or compare the behavior of two programs. Documentation and a tutorial are available on the CBAT website.
- The HOPE project built a variety of tools to support a security coprocessor under development at Draper and Dover Microsystems. I contributed to many pieces, including the design and implementation of a language for expressing security policies that can be enforced by the system.
- PARTS is a parser combinator library in Coq that supports abstraction to OCaml. It achieves excellent performance via partial evaluation.
- Cspgen is a tool for creating models of software in the Communicating Sequential Processes (CSP) process calculus. The tool accepts both C programs and LLVM IR as input, and writes a corresponding .csp file to disk. The output is compatible with FDR3, the Oxford CSP model checker. FDR may be used to check the model for for general properties, like deadlock freedom, divergence freedom and determinism, or may be compared with specifications written in CSP using refinement.
- Specgen is a tool for creating models of Enterprise Architect statecharts in the Communicating Sequential Processes (CSP) process calculus. The output is compatible with FDR3, the Oxford CSP model checker.
- I wrote hcross, a cross-platform, open source Haskell application for interactively solving crossword puzzles. It's effectively a free Across Lite replacement.
- As part of the Software Foundations project, I made a number of contributions to coqdoc, the documentation tool for the Coq proof assistant.
- I have contributed to and maintain libpuz, a C library for handling the Across Lite crossword puzzle file format. I have also participated in the community effort to reverse engineer and document that format, located at the same Google Code project page.
- I wrote hpuz, the Haskell bindings for the libpuz library.
- In 2007, I participated in Jane Street Capital's OCaml Summer Project. This was a great experience, and I highly recommend it. My project was pcl, a port of Haskell's popular Parsec library (monadic parser combinators) to Ocaml. Don't use this in production code - there are now much better options for parser combinators in OCaml.