Computer Science Division
Electrical Engineering and Computer Science Department
University of California, Berkeley
I finished my PhD in Computer Science in 2007. My research area is programming languages. My advisor was George Necula. I received a Master of Science degree in CS from Berkeley in 2004 and a Bachelor of Science in CS from CMU in 2003.
My more specific research interests are in practical applications of dependent types and interactive theorem proving to problems in programming language design and software engineering.
My PhD won't be awarded officially until December 2007, and I'm on filing fee until that time (sort of like being an undead zombie PhD student who gets rapped on the knuckles with a ruler if he tries to do anything but file a dissertation), but, as of September 17, I've moved to New York City and started working full-time at Jane Street Capital hacking OCaml for financial trading systems. Watch this space for a forwarding pointer to the new home of my research web site!
My thesis research centered on building programming language tools with proofs of total correctness, using the Coq proof assistant. What distinguishes my approach is that I use dependent types in the implementations of the tools, not just their correctness proofs, following a kind of "correctness by construction" discipline. These are some of the largest dependently-typed programming projects that I'm aware of.
Individual projects include:
|A certified type-preserving compiler from lambda calculus to assembly language, described in my PLDI'07 paper. This project has also produced a library in support of formalizing programming languages with dependently-typed abstract syntax and denotational semantics.|
|Certified program verifiers, described in my ICFP'06 paper. I've developed a component architecture for rapid construction of new certified verifiers for x86 machine code, based on functors for translating verifiers between levels of abstraction.|