Ben Delaware's Research

refereed publications

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).
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).
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).
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).
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 (FOAL) 2009.

drafts + manuscripts

technical reports + theses

Feature Modularity in Mechanized Reasoning
- Benjamin Delaware
- PhD Dissertation, University of Texas at Austin, December 2013.
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 Proposal, University of Texas at Austin, February 2013.
Bagahk: Developing Sound and Complete Decision Procedures in Coq
- Benjamin Delaware
- Master's Thesis, Washington University in St. Louis. August 2007.

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