POPL 2017
Sun 15 - Sat 21 January 2017
Adam Chlipala

Registered user since Sun 23 Nov 2014

Name:Adam Chlipala

Adam Chlipala joined the MIT faculty in 2011, after finishing his BS in computer science at Carnegie Mellon in 2003, PhD in computer science at UC Berkeley in 2007, and postdoc at Harvard. He works on designing and implementing new tools and infrastructure to support applications of computers. Most projects use the Coq proof assistant to establish correctness of systems, and one of his main obsessions is how to apply scripted proof automation and other techniques to promote readability and maintainability of large certified systems, spanning the abstraction gap from hardware designs to low-level programs like operating-system kernels to high-level application logic as with clients of relational databases. He also works in the design and implementation of functional programming languages, as in the example of his domain-specific programming language Ur/Web, which brings strong mathematical guarantees to the world of Web applications.

Country:United States
Research interests:Applications of machine-checked proofs in implementing, compiling, verifying, and/or synthesizing software & hardware; design and implementation of typed functional programming languages


Show activities from other conferences

POPL 2017-profile
View general profile