E-mail: adam@chlipala.net
I finished my PhD in Computer Science at Berkeley in 2007. I received a Master of Science degree in CS from Berkeley in 2004 and a Bachelor of Science in CS from CMU in 2003.
I'm currently doing a part-time postdoc with Greg Morrisett at Harvard. In the other half of my time, I'm working on a stealth-mode Internet start-up company built around type theory.
One of my primary research interests is engineering issues in interactive computer theorem proving, especially as related to the formal semantics of programming languages. Over the years, software developers have settled upon techniques that promote long-term maintainability of software. The field of mechanized theorem-proving sorely lacks its own counterpart. Most mechanized proofs are hard to write, understand, and evolve. We should be writing our machine-checked proofs in a way that makes them easy to adapt to changing specifications, following a standard lesson of software development. My research on computer theorem proving focuses on techniques for rapid construction of readable, automated proofs (especially in Coq), without giving up the expressivity of higher-order logic.
I'm also interested in the design and implementation of statically-typed functional programming languages, especially those with interesting facilities for type-level computation. I'm working on the Ur/Web programming language and compiler, which make it possible to generate large parts of dynamic web applications with statically-typed metaprogramming.