Adam Chlipala - Research Interests & Projects

Executive Summary

As recently as the 1980s, it was normal for "real-world" programmers to laugh at the idea of structured programming languages with such arcane features as "while" loops, as opposed to the jump instructions of assembly languages. How could a program written in a structured language possibly perform well enough, compared to hand-written assembly language? Those crazy academics are at it again, with their nutty theories. Of course, today the abstraction of structured control flow is ubiquitous. Data abstraction was another that seemed esoteric at first but has become completely standard now. Serious programmers today will laugh at anyone who uniformly writes off these techniques that seemed like theoretical distractions in 1980.

The driving thesis of my research is that machine-checked mathematical proofs are the next big enabler of practical program structuring techniques. Most observers today think that formal methods are academic curiosities that will never reduce software development costs so much that it seems silly not to use them. Those observers are as wrong as the 1980 critics of structured programming.

The serious programs of 2050 will rely on formal specifications and proofs the way that Java programs today rely on static types and interfaces. We know that our only hope to build complex systems is to find ways to break them into smaller systems, with effective ways to think about parts in isolation, viewing their dependencies abstractly through interfaces, formal or not. Proof assistant systems like Coq provide the ultimate level of flexibility and rigor in formulating decomposition strategies. Decades from now, this kind of formal reasoning will be as essential as the operating-systems abstractions developed starting in the 1950s. I've often felt jealous of the pioneers who had the chance to contribute to the science of computer systems in that time period, but I feel like those of us getting started today have a second shot at it, designing system structuring principles based on mechanized proof.

My research group is gradually building a proof-of-concept development ecosystem. Our results so far span the abstraction spectrum from mathematical specifications to functional programs to hardware circuits. Some pieces we have already connected together. Others are separate at the moment, but the end goal is to connect everything together into the computing platform of the future, replacing the ideas embodied today in, say, a Linux system running on commodity hardware, including the source code used to construct all of its pieces. This future system would be:

Current Projects

With Published Papers

Hot Off the Presses

Gauging Fit in My Group

Interested in joining the group or otherwise collaborating? Feel free to contact me if you have questions about what we could work together on. In recruiting students and postdocs, I'm generally looking for solid background in both implementation and theory. Experience with statically typed functional programming languages like OCaml and Haskell is also pretty important, and Coq experience is useful. I'll at least want to be convinced that potential students can get up to speed quickly with both kinds of tools, and the best way to do that is get started using them and show me something that you've built!

A good online introduction to Coq is Software Foundations (many undergraduates hunker down and learn from it independently over a summer or so), and my book introduces Coq for a more advanced audience, covering more of the tricky features that pay off in large developments.