Benjamin Delaware

305 N. University Street
West Lafayette, IN 47907
bendy at purdue.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

Employment

Purdue University
Associate Professor	2026-Now
Assistant Professor	2016-2026
Massachusetts Institute of Technology
Research Scientist	2015-2016
Programming Languages and Verification Group
Postdoctoral Researcher	2014-2015
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

[26] Trace-Guided Synthesis of Effectful Test Generators
- Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan
- Proceedings of the 47th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'26).
[25] LLM-Assisted Synthesis of High-Assurance C Programs
- Prasita Mukherjee, Minghai Lu, and Benjamin Delaware
- Proceedings of the 40th IEEE/ACM International Conference on Automated Software Engineering (ASE 2025).
[24] We've Got You Covered: Type-Guided Repair of Incomplete Input Generators
- Patrick LaFontaine, Zhe Zhou, Ashish Misra, Suresh Jagannathan, and Benjamin Delaware
- Proceedings of the ACM on Programming Languages, Volume 9 (OOPSLA 2025).
[23] KestRel: Relational Verification Using E-Graphs for Program Alignment
- Rob Dickerson, Prasita Mukherjee, and Benjamin Delaware
- Proceedings of the ACM on Programming Languages, Volume 9 (OOPSLA 2025).
- Recipient of a Distinguished Artifact Award.
[22] Proof Automation with Large Language Models
- Minghai Lu, Benjamin Delaware, and Tianyi Zhang
- Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024).
[21] A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
- Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan
- Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'24).
[20] Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
- Qianchuan Ye and Benjamin Delaware
- Proceedings of the ACM on Programming Languages, Volume 8 (OOPSLA 2024).
[19] Covering All the Bases: Type-based Verification of Test Input Generators
- Zhe Zhou, Ashish Misra, Benjamin Delaware, and Suresh Jagannathan
- Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'23).
- Recognized as a Distinguished Paper.
[18] Taype: a Policy-Agnostic Language for Oblivious Computation
- Qianchuan Ye and Benjamin Delaware
- Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'23).
[17] A Type-Based Approach to Divide-And-Conquer Recursion in Coq
- Pedro Abreu , Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garret Morris , and Aaron Stump,
- Proceedings of the 50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'23 ).
[16] RHLE: Modular Deductive Verification of Relational ∀∃-Properties
- Rob Dickerson, Qianchuan Ye, Michael K. Zhang Benjamin Delaware
- Proceedings of the 20th Asian Symposium on Programming Languages and Systems (APLAS'22 ).
[15] Oblivious Algebraic Datatypes
- Qianchuan Ye, Benjamin Delaware
- Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'22 ).
[14] HACCLE: Metaprogramming for Secure Multi-party Computation
- Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni
- Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts & Experiences (GPCE'21).
[13] Data-Driven Abductive Inference of Library Specifications
- Zhe Zhou, Rob Dickerson, Benjamin Delaware, Suresh Jagannathan
- Proceedings of the 2021 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'21).
- Recipient of a Distinguished Artifact Award.
[12] Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring
- Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
- Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21).
[11] Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Clément Pit--Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
- Proceedings of the 2020 International Joint Conference on Automated Reasoning (IJCAR'20).
[10] Clotho: Directed Test Generation for Weakly Consistent Database Systems
- Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
- Proceedings of the 2019 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'19).
[9] Narcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formats
- Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
- Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP'19).
[8] A Verified Protocol Buffer Compiler
- Qianchuan Ye, Benjamin Delaware
- Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'19).
[7] Using Coq to Write Fast and Correct Haskell
- John Wiegley, Benjamin Delaware
- ACM SIGPLAN Haskell Symposium 2017 (Haskell'17).
[6] The End of History? Using a Proof Assistant to Replace Language Design with Library Design
- Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit--Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
- The 2nd Summit on Advances in Programming Languages (SNAPL'17).
[5] Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
- Benjamin Delaware, Clément Pit--Claudel, Jason Gross, Adam Chlipala
- Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15).
[4] Modular Monadic Meta-Theory
- Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira
- Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP'13).
[3] Meta-Theory à la Carte
- Benjamin Delaware, Bruno C. d. S. Oliveira, Tom Schrijvers
- Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13).
[2] Product Lines of Theorems
- Benjamin Delaware, William R. Cook, Don Batory
- Proceedings of the 2011 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'11).
[1] Fitting The Pieces Together: A Machine-Checked Model of Safe Composition
- Benjamin Delaware, William R. Cook, Don Batory
- Proceedings of the 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'09).
- Preliminary version presented at Foundations of Aspect-Oriented Languages 2009 (FOAL'09).

drafts + manuscripts

technical reports + theses

Strategic Programming by Model Interpretation and Partial Evaluation
- William R. Cook, Benjamin Delaware, Thomas Finsterbusch, Ali Ibrahim, Ben Wiedermann
- Technical Report TR-09-09, UT Austin Department of Computer Sciences.
Feature Modularity in Mechanized Reasoning
- Benjamin Delaware
- PhD Dissertation, University of Texas at Austin, December 2013.
Bagahk: Developing Sound and Complete Decision Procedures in Coq
- Benjamin Delaware
- Master's Thesis, Washington University in St. Louis. August 2007.

Academic Service

Organization

Program Committee Co-Chair, International Workshop on Rocq for Programming Languages (RocqPL)	2026
Program Committee Co-Chair, International Workshop on Coq for Programming Languages (CoqPL)	2025
Diversity, Equity, and Inclusion Chair, Principles of Programming Languages (POPL)	2023
Artifact Evaluation Co-Chair, Principles of Programming Languages (POPL)	2020
Artifact Evaluation Co-Chair, Principles of Programming Languages (POPL)	2019
Student Research Competition Chair, Principles of Programming Languages (POPL)	2018

Committee Member

ACM SIGPLAN International Conference on Functional Programming (ICFP)	2026
Program Committee
The 1st International Workshop on Language Models and Programming Languages (LMPL)	2025
Program Committee
Programming Language Design and Implementation (PLDI)	2025
Program Committee
Object-Oriented Programming Systems Languages and Applications (OOPSLA)	2024
Review Committee
Programming Language Design and Implementation (PLDI)	2023
Program Committee
Principles of Programming Languages (POPL)	2023
Program Committee
Certified Programs and Proofs (CPP)	2022
Program Committee
Asian Symposium on Programming Languages and Systems (APLAS)	2020
Program Committee
Workshop on Language-Theoretic Security	2020
Program Committee
Haskell Symposium	2019
Program Committee
Object-Oriented Programming Systems Languages and Applications (OOPSLA)	2019
External Review Committee
Principles of Programming Languages (POPL)	2019
Program Committee
Asian Symposium on Programming Languages and Systems (APLAS)	2018
Program Committee
Symposium on the Implementation and Application of Functional Languages (IFL)	2018
Program Committee
Asian Symposium on Programming Languages and Systems (APLAS)	2017
Program Committee
Workshop on Feature-Oriented Software Development (FOSD)	2017
Program Committee
Principles of Programming Languages (POPL)	2017
External Review Committee
Syntax and Semantics of Low-Level Languages (LOLA)	2016
Program Committee
International Conference on Modularity,	2016
External Review Committee
Object-Oriented Programming Systems Languages and Applications (OOPSLA),	2013
Artifact Evaluation Committee

Reviewing

Principles of Programming Languages (POPL)	2024
ACM Transactions on Software Engineering and Methodology (TOSEM)	2023
Certified Programs and Proofs (CPP)	2023
Programming Language Design and Implementation (PLDI)	2022
European Symposium on Programming (ESOP)	2022
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 Software Engineering and Methodology (TOSEM)	2010

Grants

PI, SHF: Small: Automated Verification and Synthesis of Input Generators in Property-Based Testing Frameworks	2023-2026
National Science Foundation
PI, Language Support for Precise Privacy-Preserving Computation	2022-2023
Cisco
co-PI, BISON: The Zen of Cyber-Secure Serialization and Deserialization Code (STTR Phase II)	2021-2022
Department of the Air Force - Small Business Innovation Research Program
co-PI, BISON: The Zen of Cyber-Secure Serialization and Deserialization Code (STTR Phase I)	2021-2021
Department of the Air Force - Small Business Innovation Research Program
PI, Automatic Verification of k-Liveness Properties	2019-2020
Purdue Research Foundation
co-PI, HACCLE: High-Assurance Compositional Cryptography: Languages and Environments	2019-2024
IARPA
PI, CRII: SHF: Bespoke Data Representation Synthesis via Contextual Data Refinement	2018-2020
National Science Foundation (CCF-1755880)
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

instructor

CS 560: Reasoning About Programs, Purdue University	Fall 2025
	Fall 2024
	Fall 2023
CS 456: Programming Languages, Purdue University	Spring 2024
	Fall 2022
	Fall 2021
	Spring 2018
CS 565: Programming Languages, Purdue University	Spring 2022
	Fall 2020
	Fall 2018
	Fall 2016
CS 307: Software Engineering, Purdue University	Spring 2019
CS 592: Advanced Topics in Types and Programming Languages, Purdue University	Spring 2023
CS 590: Relational Program Reasoning, Purdue University	Spring 2020
CS 590: Software Synthesis, Purdue University	Spring 2017

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 2006,
	Fall 2005

Advising

Prasita Mukherjee, PhD	2023--current
Patrick LaFontaine, PhD	2022--current
Rob Dickerson, PhD	2018--current
Zhe Zhou (Co-supervised with Suresh Jagannathan), PhD	2019--current
Qianchuan Ye, PhD	2017--2024
Pedro da Costa Abreu, MSc	2018--2024
Kia Rahmani (Co-supervised with Suresh Jagannathan), PhD	2017--2022
Eric Bond, MSc	2019--2020
Ammar Askar, B.S.	2018--2019
Paul Krogmeier, MSc	2017--2018

Honors + Awards

SIGPLAN Distinguished Reviewer	2024
OOPSLA 2024
SIGPLAN Distinguished Reviewer	2023
PLDI 2023
SIGPLAN Distinguished Paper	2023
PLDI 2023
College of Science Team Award (w/ Roopsha Samanta and Tiark Rompf)	2019
Purdue University
CRII Award	2018
National Science Foundation
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

Benjamin Delaware

Organization

Committee Member

Reviewing

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

Modular Monadic Meta-Theory

Meta-Theory à la Carte

Product Lines of Theorems

Engineering Modular Mechanized Metatheory

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