Benjamin Delaware

  • 32 Vassar Street, 32-G822
  • Cambridge MA, USA 02138
  • bendy at csail.mit.edu
Education
University of Texas at Austin, Ph.D. Computer Science 2013
Advisors: William Cook and Don Batory
Dissertation: Feature Modularity in Mechanized Reasoning
Washington University in St. Louis , M.Sc. Computer Science 2007
Advisor: Aaron Stump
Thesis: Bagahk: Developing Sound and Complete Decision Procedures in Coq
Truman State University, B.S. Computer Science, B.A. Russian 2005
Summa Cum Laude with Departmental Honors in Math and Computer Science
Research Experience
Massachusetts Institute of Technology 2014-Present
Research Scientist
Programming Languages and Verification Group
Massachusetts Institute of Technology 2013-2014
Postdoctoral Researcher
Programming Languages and Verification Group
University of Texas at Austin 2007-2013
Graduate Research Assistant
Washington University in St. Louis 2006-2007
Graduate Research Assistant
Papers
refereed conference publications
drafts + manuscripts
technical reports + theses
Academic Service

  • Committee Member

  • International Conference on Modularity, External Review Committee 2016
    Object-Oriented Programming Systems Languages and Applications (OOPSLA), Artifact Evaluation Committee 2013

  • Reviewing

  • ACM Transactions on Programming Languages and Systems (TOPLAS) 2014
    Symposium On Applied Computing (SAC) 2014
    Object-Oriented Programming Systems Languages and Application (OOPSLA) 2013, 2012
    European Conference on Object-Oriented Programming (ECOOP) 2013, 2008
    Journal of Functional Programming (JFP) 2013
    Acta Informatica 2011
    International Conference on Functional Programming (ICFP) 2011
    International Conference on Objects, Models, Components and Patterns (TOOLS) 2011, 2010
    ACM Transactions on So ware Engineering and Methodology (TOSEM) 2010
Grants
Key Personnel, BRASS RINGS: Adaptability is the Prize 2015-2020
DARPA
Key Personnel, Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover 2015-2019
NSF, CCF-1512611
Teaching
assistant instructor
CS105: PHP + SQL , University of Texas at Austin Spring 2013, Fall 2013
teaching assistant
CS 378: Software Design , University of Texas at Austin Fall 2012, Spring 2010
CS 240: Logic and Discrete Mathematics , Washington University in St. Louis Spring 2007, Spring 2006
CS 511A: Introduction to AI, Washington University in St. Louis Fall 2005, Fall 2006
Mentoring
Sorawit Suriyakarn, EECS Advanced Undergraduate Research Program 2014-Present
Katherine Ye, Summer Internship with PLV Group 2015
Clément Pit--Claudel, Summer Internship with PLV Group 2014
Honors + Awards
James C. Browne Graduate Fellowship 2013
University of Texas at Austin
MCD Doctoral Fellowship 2007-2010
University of Texas at Austin
Dean's Excellence Award, College of Natural Sciences 2007
University of Texas at Austin
Distinguished Master's Fellowship 2005-2006
Washington University in St. Louis
Phi Beta Kappa 2004
Truman State University
Presidential Leadership Scholarship 2001-2005
Truman State University
Presentations

  • Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

  • University of California, Los Angeles, Seminar January 2016
    42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Conference Talk January 2015
    University of California, Berkeley (Chaperone Group), Seminar October 2014
    Stanford University (Software Research Group), Seminar October 2014

  • Modular Monadic Meta-Theory

  • 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), Conference Talk September 2013

  • Meta-Theory à la Carte

  • 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Conference Talk January 2013
    University of Ghent, Seminar December 2012

  • Product Lines of Theorems

  • 26th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Conference Talk October 2011
    2nd Conference on Interactive Theorem Proving (ITP), Joint Keynote with Don Batory August 2011

  • Engineering Modular Mechanized Metatheory

  • Dagstuhl Seminar on Feature-Oriented So ware Development, Invited Talk January 2011

  • Fitting the Pieces Together: A Machine-Checked Model of Safe Composition

  • The 7th Joint European So ware Engineering Conference and Foundations of So ware Engineering (ESEC/FSE), Conference Talk August 2009
    Foundations of Aspect-Oriented Languages (FOAL), Workshop Talk March 2009