CV - Adam Chlipala

Research interests

  • Program verification (verifying low-level programs, verifying programming language tools, reducing the human costs of interactive theorem-proving and formal verification)
  • Design and implementation of programming languages (functional and declarative programming languages, dependent types and other very expressive type systems, safe low-level programming, Web programming, domain-specific languages)

    • Education

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

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

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

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

    Employment

    Assistant Professor of Electrical Engineering and Computer Science
    7/2011 - ??
    Douglas T. Ross (1954) Career Development Professor of Software Technology
    7/2012 - ??
    Computer Science and Artificial Intelligence Laboratory
    Department of Electrical Engineering and Computer Science
    Massachusetts Institute of Technology

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

  • Led a reimplementation of the Ynot system, with a focus on proof automation
  • Research on cost-effective program verification

    • 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

  • Investigated implementation of program verification tools with proofs of correctness, using dependent types in the Coq proof assistant
  • Implemented infrastructure for the Open Verifier and Certified Program Verifiers systems
  • Developed untrusted plug-ins for memory safety of x86 Typed Assembly Language for those systems, including soundness proofs in the Coq proof assistant

    • 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

  • Designed and implemented an extensible bytecode verifier based on linear logic, and used this verifier to check properties such as manual memory management and message-passing protocols for untrusted process code in the Singularity operating system

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

  • Ran discussion sections
  • Graded weekly homework assignments
  • Held office hours

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

  • Implemented processing for an intuitive language for specifying safety properties of C programs to be verified by the BLAST model checker
  • Implemented context-free reachability to extend BLAST to verify recursive programs

    • 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

  • Implemented improvements to the mid-level intermediate language of the TILT compiler, along with assorted optimizations
  • Studied the problem of efficient type-checking of ML-like intermediate languages in flattened forms analogous to traditional compiler intermediate languages

    • 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

  • Taught a weekly recitation section
  • Created homework assignments and exam questions
  • Held weekly office hours
  • Graded assignments and exams

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

  • Developed a database-driven intranet web site to facilitate technology transfer between research and development

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

  • Designed and coded business and presentation logic for electronic commerce web sites using IBM WebSphere Commerce Suite

    • Professional service

  • National Science Foundation, panelist, 2012, 2013
  • Functional Programming Concepts in Domain-Specific Languages (FPCDSL'13), program committee
  • 8th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'13), program committee
  • 22nd USENIX Security Symposium (USENIX Security'13), program committee
  • Interactive Theorem Proving - Fourth International Conference (ITP'13), program committee
  • 43th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'13), DCCS program commitete
  • ACM SIGPLAN 2013 Conference on Programming Language Design and Implementation (PLDI'13), external review committee
  • 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'13), program committee
  • Data Driven Functional Programming Workshop 2013 (DDFP'13), program committee
  • 15th International Symposium on Practical Aspects of Declarative Languages (PADL'13), program committee
  • 2nd International Conference on Certified Programs and Proofs (CPP'12), program committee
  • 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'12), program co-chair
  • Interactive Theorem Proving - Third International Conference (ITP'12), program committee
  • The Fourth Coq Workshop (Coq-4), program chair
  • 24th International Conference on Computer Aided Verification (CAV'12), program committee
  • IEEE Symposium on Security & Privacy 2012 (S&P'12), poster chair
  • 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), program committee
  • 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), program committee
  • 16th ACM SIGPLAN International Conference on Functional Programming (ICFP'11), program committee
  • 6th International Workshop on Systems Software Verification (SSV'11), program committee
  • The Third Coq Workshop (Coq-3), program committee
  • Workshop on Foundations of Computer Security (FCS'11), program committee
  • 5th International Workshop on Systems Software Verification (SSV'10), program committee
  • Mathematically Structured Functional Programming 2010 (MSFP'10), program committee
  • The Second Coq Workshop (Coq-2), program committee
  • Programming Languages meets Program Verification Workshop (PLPV'10), program committee
  • 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'09), program committee
  • 3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM'08), program committee
  • External reviewer for: ICFP'04, LPAR'05, LICS'06, APLAS'06, TLDI'07, RTA'07, POPL'08, VMCAI'08, PLDI'08, ICFP'08, POPL'09, TLDI'09, ESOP'09, TYPES'08, PLDI'09, ICFP'09, POPL'10, FoSSaCS'10, TACAS'10, MFPS'10, PPDP'10, HOR'10, ICFP'10, POPL'11, VMCAI'11, ESOP'11, PLDI'11, RTA'11, GCM'10, VSTTE'12, FoSSaCS'12, Haskell'12, LFCS'13
  • Referee for: ESL, FI, HOSC, IPL, JACM, JAR, JFP, JFR, SCP, TOPLAS
  • External PhD thesis reviewer for: Wilmer Ricciotti-(U. of Bologna)

    • Academic honors

  • National Science Foundation CAREER Award, 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

    • Summer schools

  • Summer School on Software Security: Theory to Practice, University of Oregon, 6/2004

    • Open Source software

  • Ur/Web, a domain-specific programming language design and implementation supporting metaprogramming of web applications with strong static guarantees
  • Cooperative Internet hosting tools, including DomTool, a domain-specific language in support of shared UNIX system configuration by mutually-untrusting users
  • Dynamic web site tools for Standard ML, including separately usable libraries for accessing SQL databases

    • Other activities

  • Founder of HCoop, Inc., a democratically-run Internet hosting cooperative
  • Main administrator and organizer, Teen Programmers Unite, 1997-2001

    • Publications

    Books

    Adam Chlipala. Certified Programming with Dependent Types. To appear from MIT Press. Available online under a Creative Commons license.

    Refereed journal articles

    Adam Chlipala. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning (JFR). 3(2). 1-93, 2010.

    Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming (JFP). 18(5/6). 599-647, 2008. Cambridge University Press.

    Refereed conference papers

    Thomas Braibant, Adam Chlipala. Formal Verification of Hardware Synthesis. Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13). 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 (PLDI'11). 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 (OSDI'10). 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 (PLDI'10). 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 (POPL'10). 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 (ICFP'09). August 2009.

    Adam Chlipala. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08). 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 (PLDI'07). 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 (ICFP'06). 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 (VMCAI'06). 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 (ICSE'04), IEEE Computer Society Press. May 2004.

    Refereed workshop papers

    Adam Chlipala. Position Paper: Thoughts on Programming with Proof Assistants. Proceedings of the Programming Languages meets Program Verification Workshop (PLPV'06). 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 (STRATEGIES'06). 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 (TLDI'05). 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 (TLDI'05). 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 (TLDI'05). January 2005.

    Refereed poster sessions

    Adam Chlipala. Developing Certified Program Verifiers with a Proof Assistant. Proceedings of the International Workshop on Proof-Carrying Code (PCC'06). 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 (SAS'04), 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.

    Adam Chlipala. Implementing Certified Programming Language Tools in Dependent Type Theory. Technical Report UCB/EECS-2007-113. 2007.

    Adam Chlipala. Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types. Technical Report UCB/EECS-2006-120. 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.

    Adam Chlipala. An Untrusted Verifier for Typed Assembly Language. MS Project Report. Technical Report UCB/ERL M04/41. UC Berkeley EECS Department. 2004.

    Talks

    A Taste of Effective Coq Proof Automation (invited tutorial). POPL'13 TutorialFest. January 2013.

    Web Security via Types and Theorem-Proving in the Ur/Web Programming Language. CSAIL Student Workshop. September 2011.

    Web Security via Types and Theorem-Proving in the Ur/Web Programming Language. IBM Watson Research Center. August 2011.

    Bedrock: Higher-Order and Automated Proofs about Low-Level Programs (invited talk). LOLA'11. June 2011.

    Ur/Web, a Domain-Specific Functional Programming Language for Modern Web Applications. UC Berkeley. June 2011.

    Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. PLDI'11. June 2011.

    Ur/Web, a Domain-Specific Functional Programming Language for Modern Web Applications. MIT PL Working Group. December 2010.

    Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. OSDI'10. October 2010.

    Foundational Program Verification in Coq with Automated Proofs (invited tutorial). MSFP'10. September 2010.

    Cost-Effective and Foundational Verification of Low-Level Code. Dagstuhl Seminar #10351. August 2010.

    Ur/Web, a Domain-Specific Functional Programming Language for Modern Web Applications. COPLAS, ITU Copenhagen. August 2010.

    Ur/Web: A Statically-Typed Language for Building Web Applications from Components (invited talk). Emerging Languages Camp 2010. July 2010.

    A Bottom-Up Approach to Safe Low-Level Programming (invited talk). MLPA'10. July 2010.

    Generating Pieces of Web Applications with Type-Level Programming. DTP'10. July 2010.

    Ur: Statically-Typed Metaprogramming with Type-Level Record Computation. PLDI'10. June 2010.

    Safe Database Abstractions with Type-Level Record Computation (invited talk). RADICAL'10. May 2010.

    A Sane Approach to Modern Web Application Development. Boston Lisp. February 2010.

    A Verified Compiler for an Impure Functional Language. POPL'10. January 2010.

    Towards the Ultimate Web Application Framework, via Fancy Types. New England F# User Group. November 2009.

    Syntactic Proofs of Compositional Compiler Correctness. NJPLS. October 2009.

    Metaprogramming AJAX Apps with Static Types. DEFUN'09. September 2009.

    Engineering a Verified Functional Language Compiler (invited talk). WMM'09. September 2009.

    Effective Interactive Proofs for Higher-Order Imperative Programs. ICFP'09. August 2009.

    Metaprogramming AJAX Apps with Static Types. Microsoft Research Redmond. July 2009.

    Liberating Semi-Automated PL Proofs from Binder Bookkeeping. Northeastern University Programming Languages Seminar. February 2009.

    Liberating Semi-Automated PL Proofs from Binder Bookkeeping. Boston University Programming Languages Reading Group. February 2009.

    Statically-Checked Metaprogramming for Web Applications. NEPLS 21. November 2008.

    Parametric Higher-Order Abstract Syntax for Mechanized Semantics. ICFP'08. September 2008.

    Generic Programming and Proving for Programming Language Metatheory. WMM'07. October 2007.

    A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. PLDI'07. June 2007.

    A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Open Source Quality Project Retreat. May 2007.

    A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Projet Gallium seminar. January 2007.

    Modular Development of Certified Program Verifiers with a Proof Assistant. ICFP'06. September 2006.

    Position Paper: Thoughts on Programming with Proof Assistants. PLPV'06. August 2006.

    Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. STRATEGIES'06. August 2006.

    Developing Sound Program Analysis Tools by Programming with Proofs. Open Source Quality Project Retreat. May 2006.

    A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. VMCAI'06. January 2006.

    Proof-Carrying Verifiers. Open Source Quality Project Retreat. May 2005.

    The Open Verifier Framework for Foundational Verifiers. TLDI'05. January 2005.

    Research funding

  • CAREER: A Formal Verification Platform Focused on Programmer Productivity, NSF CCF
  • SHF: Small: Capitalizing on First-Class SQL Support in the Ur/Web Programming Language, NSF CCF
  • CAP3: A Computer Aided Performance Programming Platform, DoE X-Stack program
  • CARS: A Platform for Scaling Formal Verification to Component-Based Vehicular Software Stacks, DARPA HACMS program
  • Safe but Unsandboxed Native Code in the Browser, Google Research Award