Adam Chlipala 579 Soda Hall Computer Science Division University of California, Berkeley Berkeley, CA 94720-1776 USA adamc@cs.berkeley.edu http://www.cs.berkeley.edu/~adamc/ ========= 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 =============== * 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 ========== * 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 * 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 ==================== * 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 * Laconic/Web (http://laconic.sourceforge.net/), 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 (http://smlweb.sourceforge.net/), including separately usable libraries for accessing SQL databases ================ Other activities ================ * Founder and President of HCoop, Inc. (http://hcoop.net/), a democratically-run Internet hosting cooperative * Black belt in Karate (no longer training) ============ 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. 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 journal articles: * Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming. 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. 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.