Adam Chlipala PhD alumnus E-mail: adamc@cs.berkeley.edu 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.

• Proof-carrying code
• Interactive computer theorem proving
• Program analysis
• Software model checking
• Typed compiler intermediate languages

• My publications
• As BibTeX
• My CV
• In PostScript
• In PDF
• Resumé, for jobs outside computer science research (PDF)
• Classes I've taken
• LinkedIn profile

• The certified programming language tools described at the top of this page have open source implementations that generate executable OCaml code.
• Cooperative Internet hosting tools, including DomTool, a domain-specific language in support of shared UNIX system configuration by mutually-untrusting users
• Laconic/Web, a prototype domain-specific programming language design and implementation supporting meta-programming of web applications with strong static guarantees
• Dynamic web site tools for Standard ML, including separately usable libraries for accessing SQL databases
• Links to sundry other projects can be found from my SourceForge profile.
• Most of this web site is built from an XML database using XSLT. I've published my code for doing this.

• Course on Interactive Computer Theorem Proving (focusing on Coq) that I taught in Fall 2006
• A point-by-point comparison of the Objective Caml and Standard ML programming languages
• Looking for Internet hosting where you can go wild developing Internet services with your favorite non-mainstream programming language? Join HCoop, the Internet Hosting Cooperative!
• My personal web site
• Best upper bound on my Erdös Number that I know of: 4

View of San Francisco from my office desk