![]() |
Adam Chlipala E-mail: adamc@hcoop.net I finished my PhD in Computer Science at Berkeley in 2007. My research interests center on programming languages and computer theorem proving. 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. |
Starting with my thesis research, I've been developing the Lambda Tamer library for programming language formalization in Coq. I'm working towards a certified compiler for core ML; that is, a compiler with a machine-checked proof that it preserves program meanings. I follow a somewhat unusual style, including a few key elements:
Relevant recent papers: