Adam Chlipala

Adam Chlipala is the Arthur J. Conner Professor of Computer Science at MIT, with appointments in the Computer Science and Artificial Intelligence Laboratory (CSAIL) and the Department of Electrical Engineering and Computer Science. His research integrates programming languages and formal methods to develop verified computer systems.

Education:

• PhD in Computer Science, University of California, Berkeley
• MS in Computer Science, University of California, Berkeley
• BS in Computer Science, Carnegie Mellon University

Research Focus: Dr. Chlipala's work spans:

• Verified compilers and programming tools
• Cryptographic protocol implementation
• Hardware description languages
• Proof automation in theorem provers
• High-performance parallel computing

His current projects focus on rethinking abstractions for parallel systems with end-to-end formal verification.

Teaching: He has created and teaches courses on verified software engineering (6.S057), programming fundamentals (6.1010), and formal reasoning about programs (6.5120). His educational materials include textbooks on Certified Programming with Dependent Types and Formal Reasoning About Programs.

Awards and Honors: His research has been recognized with the German IT Security Award, Humies Gold Award for evolutionary computation, and multiple teaching prizes including the Jamieson Prize. He is an ACM Distinguished Member and NSF CAREER awardee.

Research Teams: Dr. Chlipala leads the Programming Languages & Verification Group at MIT CSAIL. His startup Nectry develops no-code enterprise software based on the Ur/Web language and UPO proof system.