CV - Adam Chlipala

Research interests

  • Dependent type systems; interactive theorem proving; type-based programming methodologies that integrate programming with correctness proofs
  • Program verification; language-based security; proof-carrying code; typed assembly language; model checking; formal methods for low-level software
  • Design and implementation of declarative programming languages; type systems and logics; functional programming
  • Automated deduction; interactive proof assistants

    • 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

    Publications

    Refereed conference papers

    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 journal articles

    Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming (JFP). Cambridge University Press. Accepted pending revision.

    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

    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.

    Employment

    Quantitative Researcher
    Jane Street Capital
    9/2007 - present

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

  • Investigating 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

    • Academic honors

  • 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

    • Experience with 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

    Summer schools

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

    • External reviewer for:

    ICFP'04, LPAR'05, LICS'06, APLAS'06, TLDI'07, RTA'07, POPL'08, VMCAI'08

    Open Source software

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

    • Other activities

  • Founder and President of HCoop, Inc., a democratically-run Internet hosting cooperative
  • Black belt in Karate (no longer training)