Computer Science Assistant
Resume:
Adam Chlipala
Computer Science Division
University of California, Berkeley
Berkeley, CA 94720-1776
USA
*****@**.********.***
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.
Contact this candidate