Benjamin Delaware

According to our database, Benjamin Delaware authored at least 28 papers between 2009 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata.

Zhe Zhou, Qianchuan Ye, Benjamin Delaware, Suresh Jagannathan

Proc. ACM Program. Lang., 2024

Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation.

Qianchuan Ye, Benjamin Delaware

Proc. ACM Program. Lang., 2024

Proof Automation with Large Language Models.

Minghai Lu, Benjamin Delaware, Tianyi Zhang

CoRR, 2024

KestRel: Relational Verification Using E-Graphs for Program Alignment.

Robert Dickerson, Prasita Mukherjee, Benjamin Delaware

CoRR, 2024

2023

A Type-Based Approach to Divide-and-Conquer Recursion in Coq.

Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump

Proc. ACM Program. Lang., January, 2023

Covering All the Bases: Type-Based Verification of Test Input Generators.

Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan

Proc. ACM Program. Lang., 2023

Taype: A Policy-Agnostic Language for Oblivious Computation.

Qianchuan Ye, Benjamin Delaware

Proc. ACM Program. Lang., 2023

2022

Oblivious algebraic data types.

Qianchuan Ye, Benjamin Delaware

Proc. ACM Program. Lang., 2022

RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties.

Robert Dickerson, Qianchuan Ye, Michael K. Zhang, Benjamin Delaware

Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021

Data-driven abductive inference of library specifications.

Zhe Zhou, Robert Dickerson, Benjamin Delaware, Suresh Jagannathan

Proc. ACM Program. Lang., 2021

Relational Type Theory (All Proofs).

Aaron Stump, Benjamin Delaware, Christopher Jenkins

CoRR, 2021

Repairing serializability bugs in distributed database programs via automated schema refactoring.

Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

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, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni

Proceedings of the GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17, 2021

2020

HACCLE: An Ecosystem for Building Secure Multi-Party Computations.

Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni

CoRR, 2020

RHLE: Automatic Verification of ∀∃-Hyperproperties.

Robert Dickerson, Qianchuan Ye, Benjamin Delaware

CoRR, 2020

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 Automated Reasoning - 10th International Joint Conference, 2020

2019

CLOTHO: directed test generation for weakly consistent database systems.

Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan

Proc. ACM Program. Lang., 2019

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats.

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala

Proc. ACM Program. Lang., 2019

A verified protocol buffer compiler.

Qianchuan Ye, Benjamin Delaware

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats.

Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala

CoRR, 2018

2017

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

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Using Coq to write fast and correct Haskell.

John Wiegley, Benjamin Delaware

Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, 2017

2015

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 Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2013

Meta-theory à la carte.

Benjamin Delaware, Bruno C. d. S. Oliveira, Tom Schrijvers

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Modular monadic meta-theory.

Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2011

Product lines of theorems.

Benjamin Delaware, William R. Cook, Don S. Batory

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

2009

Fitting the pieces together: a machine-checked model of safe composition.

Benjamin Delaware, William R. Cook, Don S. Batory

Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009

A machine-checked model of safe composition.

Benjamin Delaware, William R. Cook, Don S. Batory

Proceedings of the 8th Workshop on Foundations of Aspect-Oriented Languages, 2009