Benjamin Delaware
where else to find them
no profile links on file
what they talk about
all 9 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2026
- OOPSLA3 editions2021–2025
- CoqPL2 editions2022–2025
all 7 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Suresh Jagannathan16 talks
- Zhe Zhou13 talks
- Qianchuan Ye6 talks
- Adam Chlipala23 talks
- Thomas Reps20 talks
- Benjamin C. Pierce17 talks
| title | conference | date |
|---|---|---|
| Trace-Guided Synthesis of Effectful Test Generators | PLDI 2026 | 2026-06-15 |
Underapproximate type-and-effect specs (U-hats) plus a small typed DSL synthesize effectful test generators that interact with black-box systems rather than… | ||
| We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators | OOPSLA 2025 | 2025-10-16 |
A tool called Cobb repairs incomplete OCaml input generators by synthesizing code that fills typed holes so the generator’s range includes every valid input… | ||
| KestRel: Relational Verification Using E-Graphs for Program Alignment | OOPSLA 2025 | 2025-10-16 |
KestRel builds an intermediate product program via an algebra of alignments, represents the rewrite search in e-graphs and equality saturation, and extracts… | ||
| Towards Automated Verification of LLM-Synthesized C Programs | CoqPL 2025 | 2025-01-25 |
SYNVER is a pipeline that uses GPT-4 to synthesize C programs and a Verified Software Toolchain backend with an Ltac layer called SEauto to discharge proofs… | ||
| From Traces to Program Incorrectness: A Type-Theoretic Approach | TPSA 2025 | 2025-01-19 |
Claims a type-theoretic, underapproximate correctness method that treats library interactions as traces encoded with symbolic regular expressions and reasoned… | ||
| Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation | OOPSLA 2024 | 2024-10-20 |
A new MPC language called Taypsi compiles ordinary functional programs with recursive ADTs into policy-respecting oblivious implementations using a lifting… | ||
| A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…) | PLDI 2024 | 2024-06-24 |
Describes a toolchain that uses symbolic finite automata to encode data-dependent, temporal representation invariants and integrates them into a refinement… | ||
| Type-Based Incorrectness Reasoning | Incorrectness 2024 | 2024-01-17 |
Claims that coverage types extend refinement types to give underapproximate reasoning that verifies completeness of nondeterministic test generators, and shows… | ||
| Taype: A Policy-Agnostic Language for Oblivious Computation | PLDI 2023 | 2023-06-17 |
Taype provides a policy-agnostic language and a compiler that implements oblivious algebraic data types and tape semantics, translating λOADT+ concepts into a… | ||
| Covering All the Bases: Type-Based Verification of Test Input Generators | PLDI 2023 | 2023-06-17 |
Claims a new coverage types system that interprets refinements as underapproximate reasoning and verifies whether generators actually produce every value in a… | ||
| A Type-Based Approach to Divide-and-Conquer Recursion in Coq | POPL 2023 | 2023-01-15 |
Presents a type-level interface that encodes divide-and-conquer recursion as Mendler-style algebras, implemented in Coq and expressible in System F_omega plus… | ||
| Scrap your boilerplate definitions in 10 lines of Ltac! | CoqPL 2022 | 2022-01-22 |
Library IDT generates new inductive definitions from existing ones by running Template-Coq code driven by small Ltac constructor-transformer tactics, so dozens… | ||
| Oblivious Algebraic Data Types | POPL 2022 | 2022-01-16 |
Presents Lambda OADT, a dependently typed calculus that encodes recursive private data by tagging each type with a public view (e.g. max tree depth) and… | ||
| HACCLE: Metaprogramming for Secure Multi-Party Computation | GPCE 2021 | 2021-10-17 |
HACCLE is a compiler toolchain that embeds a DSL (Harpoon) in Scala, uses LMS metaprogramming to lower code to a protocol‑independent acyclic circuit IR (HIR)… | ||
| Data-Driven Abductive Inference of Library Specifications | OOPSLA 2021 | 2021-10-17 |
Tool named Elrond infers specifications for black‑box OCaml libraries by combining random testing, SMT counterexample-guided refinement, and an abduction loop… | ||
| nothing matches | ||