Adam Chlipala

Cambridge, MA
USA
adamc@csail.mit.edu
http://adam.chlipala.net/

=========
Objective
=========

Not currently seeking employment

=========
Education
=========

* University of California, Berkeley
Electrical Engineering and Computer Science Department
Computer Science Division
Doctor of Philosophy (PhD) in Computer Science
8/2003 - 9/2007
Advisor: George Necula
Cumulative GPA: 4.0 out of 4.0
Thesis: Implementing Certified Programming Language Tools in Dependent Type Theory

* University of California, Berkeley
Electrical Engineering and Computer Science Department
Computer Science Division
Master of Science (MS) in Computer Science
12/2004
Advisor: George Necula
Thesis: An Untrusted Verifier for Typed Assembly Language

* Carnegie Mellon University, Pittsburgh, PA
Bachelor of Science (BS) in Computer Science with a minor in Mathematical Sciences and University Honors
8/2000 - 5/2003
Cumulative GPA: 4.0 out of 4.0

* Emmaus High School, Emmaus, PA
High school diploma
9/1996 - 6/2000

=====================
Software technologies
=====================

* I have expert-level experience with and have hacked on implementations of: ML, Coq, C
* I've written significant amounts of code in: F#, Java, SQL, x86 and Z80 assembly languages
* I'm conversant in: Haskell, C++, XSLT
* I have some familiarity with: Twelf, Scheme, Common Lisp, Prolog, C#, Visual Basic, UNIX shell scripting, Perl
* I've done system administration of these daemons on UNIX systems with at least 100 users: Apache, djbdns, Courier IMAP, Exim, Mailman, SpamAssassin

===============
Academic honors
===============

* 
    	        Annual "Humies" Awards For Human-Competitive Results Produced By Genetic And Evolutionary Computation (Gold Award)
		https://www.human-competitive.org/
		2023
	
* 
    	        PLDI Distinguished Reviewer Award
		https://pldi23.sigplan.org/
		2023
	
* 
		Burgess (1952) & Elizabeth Jamieson Prize for Excellence in Teaching
		2023
	
* 
		ACM Distinguished Member
		https://awards.acm.org/distinguished-members
		2019
	
* 
		Ruth and Joel Spira Award for Excellence in Teaching
		https://engineering.mit.edu/faculty-research/faculty-awards/teaching-awards/
		2019
	
* 
		Most Influential ICFP Paper Award
		http://www.sigplan.org/Awards/ICFP/
		2018
	
* 
		ACM Senior Member
		https://awards.acm.org/senior-members
		2016
	
* 
		National Science Foundation CAREER Award
		http://www.nsf.gov/awardsearch/showAward?AWD_ID=1253229
		2012
	
* National Defense Science and Engineering Graduate Fellowship winner, 2004
* National Science Foundation Graduate Research Fellowship winner, 2004
* California Microelectronics Fellowship winner, UC Berkeley EECS Department,
8/2003 - 5/2004
* Inducted into Phi Kappa Phi
* Inducted into Phi Beta Kappa
* Honorable Mention, National Science Foundation Graduate Research Fellowship competition, 2003
* Andrew Carnegie Scholarship winner, Carnegie Mellon University, Pittsburgh, PA,
8/2000 - 5/2003

==========
Employment
==========

* Professor of Computer Science
Computer Science and Artificial Intelligence Laboratory
Department of Electrical Engineering and Computer Science
Massachusetts Institute of Technology
7/2022 - ??

* Postdoctoral Fellow
School of Engineering and Applied Sciences
Harvard University, Cambridge, MA
6/2008 - 6/2011
Advisor: Greg Morrisett

* Instructor
COMPSCI 252: Certified Programming with Dependent Types
School of Engineering and Applied Sciences
Harvard University, Cambridge, MA
9/2008 - 1/2009

* OCaml Hacker
Jane Street Capital
9/2007 - 4/2008

* Graduate Student Researcher
The Open Verifier project
Computer Science Division
University of California, Berkeley
9/2003 - 8/2007
PI: George Necula

* Instructor
CS294-9: Interactive Computer Theorem Proving
Computer Science Division
University of California, Berkeley
8/2006 - 12/2006

* Research Intern
The Singularity project
Software Productivity Tools group, Redmond, WA
Microsoft Research
6/2005 - 8/2005
Mentor: Manuel Fahndrich

* Graduate Student Instructor
CS172: Computability and Complexity
Computer Science Division
University of California, Berkeley
1/2005 - 5/2005
Instructor: Brian Lucena

* Graduate Student Researcher
The BLAST project
Computer Science Division
University of California, Berkeley
6/2003 - 8/2003
PI: Thomas Henzinger

* Research Assistant
The TILT type-directed Standard ML compiler project
Computer Science Department
Carnegie Mellon University, Pittsburgh, PA
6/2002 - 5/2003
PIs: Robert Harper, Karl Crary

* Teaching Assistant
15-212: Principles of Programming (introduction to formal reasoning about programs and functional programming with Standard ML)
Computer Science Department
Carnegie Mellon University, Pittsburgh, PA
1/2002 - 5/2002
Instructors: Michael Erdmann, Jeannette Wing

* Intern/Software Developer
Avaya Communication, Holmdel, NJ
6/2001 - 8/2001

* Software Developer
Trifecta Technologies, Allentown, PA
Summers, 1998 - 2000

===========
Citizenship
===========

American citizen

====================
Open source software
====================

* Ur/Web (http://www.impredicative.com/ur/), a domain-specific programming language design and implementation supporting metaprogramming of web applications with strong static guarantees
* Cooperative Internet hosting tools (http://hcoop.sourceforge.net/), including DomTool (http://wiki.hcoop.net/DomTool), a domain-specific language in support of shared UNIX system configuration by mutually-untrusting users
* Dynamic web site tools for Standard ML (http://smlweb.sourceforge.net/), including separately usable libraries for accessing SQL databases

================
Other activities
================

* Founder of HCoop, Inc. (http://hcoop.net/), a democratically run Internet hosting cooperative
* Main administrator and organizer, Teen Programmers Unite (http://www.tpu.org/), 1997-2001

============
Publications
============

Refereed journal articles:

* Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter. Omnisemantics: Smoother Handling of Nondeterminism. ACM Transactions on Programming Languages and Systems. . , 2023. 
* Thomas Gregoire, Adam Chlipala. Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. Journal of Automated Reasoning. . , 2018. 
* Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, Steve Zdancewic. The Science of Deep Specification. Philosophical Transactions of the Royal Society A. . , 2017. 
* Tej Chajed, Haogang Chen, Adam Chlipala, Frans Kaashoek, Nickolai Zeldovich, Daniel Ziegler. Research Highlight: Certifying a File System using Crash Hoare Logic: Correctness in the Presence of Crashes. Communications of the ACM. 60(4). 75-84, 2017. 
* Adam Chlipala. Research Highlight: Ur/Web: A Simple Model for Programming the Web. Communications of the ACM. 59(8). 93-100, 2016. 
* Adam Chlipala. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning. 3(2). 1-93, 2010. 
* Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming. 18(5/6). 599-647, 2008. 

Refereed conference papers:

* Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala. Foundational Integration Verification of a Cryptographic Server. Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2024. 
* Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley. A Verified Compiler for a Functional Tensor Language. Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2024. 
* Samuel Gruetter, Viktor Fukala, Adam Chlipala. Live Verification in an Interactive Proof Assistant. Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2024. 
* Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andrew Wright, Adam Chlipala. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming. September 2023. 
* Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom. CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2023. 
* Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic. C4: Verified Transactional Objects. Proceedings of the 2022 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications. November 2022. 
* Joonwon Choi, Adam Chlipala, Arvind. Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. Proceedings of the 34th International Conference on Computer-Aided Verification. August 2022. 
* Timothy Braje, Alice Lee, Andrew Wagner, Benjamin Kaiser, Daniel Park, Martine Kalke, Robert Cunningham, Adam Chlipala. Adversary Safety by Construction in a Language of Cryptographic Protocols. Proceedings of the 35th IEEE Computer Security Foundations Symposium. August 2022. 
* Jason Gross, Andres Erbsen, Miraya Poddar-Agrawal, Jade Philipoom, Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. Proceedings of the Interactive Theorem Proving - Thirteenth International Conference. August 2022. 
* Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala. Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. Proceedings of the Interactive Theorem Proving - Thirteenth International Conference. August 2022. 
* Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala. Relational Compilation for Performance-Critical Applications. Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2022. 
* Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley. Verified Tensor-Program Optimization Via High-level Scheduling Rewrites. Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2022. 
* Mirai Ikebuchi, Andres Erbsen, Adam Chlipala. Certifying Derivation of State Machines from Coroutines. Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2022. 
* Adam Chlipala. Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl). Proceedings of the 26th ACM SIGPLAN International Conference on Functional Programming. August 2021. 
* Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala. Integration Verification Across Software and Hardware for a Simple Embedded System. Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2021. 
* Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala. Effective Simulation and Debugging for a High-Level Hardware Language Using Software Compilers. Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems. April 2021. 
* Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. Proceedings of the 9th International Joint Conference on Automated Reasoning. June 2020. 
* Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind. The Essence of Bluespec: A Core Language for Rule-Based Hardware Design. Proceedings of the ACM SIGPLAN 2020 Conference on Programming Language Design and Implementation. June 2020. 
* Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala. Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats. Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming. August 2019. 
* Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala. Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises. Proceedings of the IEEE Symposium on Security & Privacy 2019. May 2019. 
* Adam Chlipala. Algorithmic Checking of Security Arguments for Microprocessors. Proceedings of the Annual GOMACTech Conference 2019. March 2019. 
* Atalay Ileri, Tej Chajed, Adam Chlipala, Frans Kaashoek, Nickolai Zeldovich. Proving confidentiality in a file system using DiskSec. Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation. October 2018. 
* Antonis Stampoulis, Adam Chlipala. Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of Lambda-Prolog/Makam. Proceedings of the 23rd ACM SIGPLAN International Conference on Functional Programming. September 2018. 
* Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin. Computable decision-making on the reals and other spaces via partiality and nondeterminism. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. July 2018. 
* Jason Gross, Andres Erbsen, Adam Chlipala. Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac. Proceedings of the Interactive Theorem Proving - Ninth International Conference. July 2018. 
* Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Ileri, Adam Chlipala, Frans Kaashoek, Nickolai Zeldovich. Verifying a High-Performance Crash-Safe File System Using a Tree Specification. Proceedings of the 26th ACM Symposium on Operating Systems Principles. October 2017. 
* Peng Wang, Di Wang, Adam Chlipala. TiML: A Functional Language for Practical Complexity Analysis with Invariants. Proceedings of the 2017 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications. October 2017. 
* Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind. Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification. Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming. September 2017. 
* Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. Proceedings of the The 2nd Summit oN Advances in Programming Languages. May 2017. 
* Ziv Scully, Adam Chlipala. A Program Optimization for Automatic Database Result Caching. Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2017. 
* Thomas Gregoire, Adam Chlipala. Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. Proceedings of the Interactive Theorem Proving - Seventh International Conference. August 2016. 
* Mohsen Lesani, Christian J. Bell, Adam Chlipala. Chapar: Certified Causally Consistent Distributed Key-Value Stores. Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2016. 
* Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, Frans Kaashoek, Nickolai Zeldovich. Using Crash Hoare Logic for Certifying the FSCQ File System. Proceedings of the 25th ACM Symposium on Operating Systems Principles. October 2015. 
* Adam Chlipala. An Optimizing Compiler for a Purely Functional Web-Application Language. Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. August 2015. 
* Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave. Modular Deductive Verification of Multiprocessor Hardware Designs. Proceedings of the 27th International Conference on Computer Aided Verification. July 2015. 
* Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2015. 
* Adam Chlipala. Ur/Web: A Simple Model for Programming the Web. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2015. 
* Adam Chlipala. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2015. 
* Peng Wang, Santiago Cuellar, Adam Chlipala. Compiler Verification Meets Cross-Language Linking via Data Abstraction. Proceedings of the 2014 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, & Applications. October 2014. 
* Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. Proceedings of the 11th USENIX Symposium on Operating System Design and Implementation. October 2014. 
* Gregory Malecha, Adam Chlipala, Thomas Braibant. Compositional Computational Reflection. Proceedings of the 5th International Conference on Interactive Theorem Proving. July 2014. 
* Jason Gross, Adam Chlipala, David Spivak. Experience Implementing a Performant Category-Theory Library in Coq. Proceedings of the 5th International Conference on Interactive Theorem Proving. July 2014. 
* Adam Chlipala. The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier. Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. September 2013. 
* Thomas Braibant, Adam Chlipala. Formal Verification of Hardware Synthesis. Proceedings of the 25th International Conference on Computer Aided Verification. July 2013. 
* Adam Chlipala. Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation. June 2011. 
* Adam Chlipala. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation. October 2010. 
* Adam Chlipala. Ur: Statically-Typed Metaprogramming with Type-Level Record Computation. Proceedings of the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation. June 2010. 
* Adam Chlipala. A Verified Compiler for an Impure Functional Language. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2010. 
* Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky. Effective Interactive Proofs for Higher-Order Imperative Programs. Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. August 2009. 
* Adam Chlipala. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. September 2008. 
* Adam Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. June 2007. 
* Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming. September 2006. 
* Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. January 2006. 
* Dirk Beyer, Adam Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. Generating Tests from Counterexamples. Proceedings of the 26th International Conference on Software Engineering, IEEE Computer Society Press (IEEE). May 2004. 

Refereed workshop papers:

* Haogang Chen, Daniel Ziegler, Adam Chlipala, Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich. Towards Certified Storage Systems. Proceedings of the 15th Workshop on Hot Topics in Operating Systems. May 2015. 
* Adam Chlipala. Position Paper: Thoughts on Programming with Proof Assistants. Proceedings of the Programming Languages meets Program Verification Workshop. August 2006. 
* Adam Chlipala, George C. Necula. Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. Proceedings of the 6th International Workshop on Strategies in Automated Deduction. August 2006. 
* Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. The Open Verifier Framework for Foundational Verifiers. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation. January 2005. 
* Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. Type-Based Verification of Assembly Language for Compiler Debugging. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation. January 2005. 
* Adam Chlipala, Leaf Petersen, Robert Harper. Strict Bidirectional Type Checking. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation. January 2005. 

Refereed poster sessions:

* Adam Chlipala. Developing Certified Program Verifiers with a Proof Assistant. Proceedings of the International Workshop on Proof-Carrying Code. August 2006. 

Invited conference papers:

* Dirk Beyer, Adam Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. The Blast Query Language for Software Verification. Proceedings of the 11th Static Analysis Symposium, Lecture Notes in Computer Science 3148, Springer-Verlag. August 2004. 

Technical reports:

* Adam Chlipala. Generic Programming and Proving for Programming Language Metatheory. Technical Report UCB/EECS-2007-147. 2007.2007.
* Adam Chlipala. Implementing Certified Programming Language Tools in Dependent Type Theory. Technical Report UCB/EECS-2007-113. 2007.2007.
* Adam Chlipala. Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types. Technical Report UCB/EECS-2006-120. 2006.2006.
* Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Technical Report UCB/ERL M05/32. UC Berkeley EECS Department. 2005.UC Berkeley EECS Department. 2005.
* Adam Chlipala. An Untrusted Verifier for Typed Assembly Language. MS Project Report. Technical Report UCB/ERL M04/41. UC Berkeley EECS Department. 2004.UC Berkeley EECS Department. 2004.