I focus on designing the computing platforms and development tools of the future, most often by using computer theorem proving to increase their simplicity, correctness, or both. Most of my work uses <a href="https://coq.inria.fr/">the Coq proof assistant</a>, which I wrote <a href="http://adam.chlipala.net/cpdt/">a book</a> on. I'm also the main designer and implementer of <a href="http://www.impredicative.com/ur/">the Ur/Web programming language for web applications</a>. Currently employed as faculty in computer science at <a href="http://www.csail.mit.edu/">MIT</a>, though I had plenty of fun building real computer systems in the 90's before it became (part of) my day job.