I currently work on programming tools for the ACL2 theorem prover such as Dracula, an interface between ACL2 and DrScheme.

I have previously worked on a compiler for Honu, a language for Interface-Oriented Programming; and on sequence traces, a tiered model of object-oriented computation.

I am also interested in functional programming, including persistent datastructures and functional reactive programming; and in various forms of lightweight program verification (i.e. less than a general purpose theorem prover), including type analysis and software contracts.

During the summer of 2005 I worked for the Sun Microsystems Programming Language Research Group on an interpreter for the Fortress programming language. During the summer of 2004 I worked at the IBM Austin Research Laboratory prototyping a typed, ML-like hardware description language.