Adam Chlipala

About

Adam's background is in programming languages and formal methods. He is interested in developing simpler and more effective abstractions for building correct, secure, and performant systems -- usually taking advantage of machine-checked mathematical proofs somehow. His work applies ideas like object-capability systems, proof-carrying code, transactions, type systems, and whole-program optimizing compilers for high-level languages; with applications in computer architecture, cryptography, databases, and operating systems, including novel designs that span traditional layers.