Benjamin C. Pierce
where else to find them
website:https://cis.upenn.edu/~bcpierce
github:bcpierce00
what they talk about
all 7 in the filters
where they keep going back
- OOPSLA2 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2026
- POPL2 editions2023–2026
all 7 in the filters
on a stage with
all 43 in the filters
who talks about the same things
- Harrison Goldstein10 talks
- Leonidas Lampropoulos15 talks
- Benjamin Delaware18 talks
- Todd Millstein11 talks
- Zain K Aamer2 talks
- Poorva Garg3 talks
| title | conference | date |
|---|---|---|
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | PLDI 2026 | 2026-06-15 |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| Typing Strictness | POPL 2026 | 2026-01-11 |
Proposes a refinement of strictness called intentional strictness and encodes it as a type-and-effect system for call-by-name and call-by-push-value, with a… | ||
| Tuning Random Generators: Property-Based Testing as Probabilistic Programming | OOPSLA 2025 | 2025-10-16 |
Generators become probabilistic programs with symbolic weights and are tuned by computing a symbolic distribution, compiling it into compressed BDD-based… | ||
| Bennet: Randomized Specification Testing for Heap-Manipulating Programs | OOPSLA 2025 | 2025-10-16 |
Bennet synthesizes C test generators from CN specifications by compiling preconditions into a DSL and running randomized backtracking search to place heap… | ||
| QED in Context: An Observation Study of Proof Assistant Users | OOPSLA 2025 | 2025-10-16 |
An observational study watches 30 proof assistant users (half Rocq and Lean) for ~1 hour each and surfaces four concrete findings: proofs evolve nonlinearly… | ||
| Mica: Automated Differential Testing for OCaml Modules | OCaml 2024 | 2024-09-07 |
Mica is a PPX extension that derives QuickCheck-based differential tests for any OCaml signature by generating a typed algebraic exper AST, a gen_xer generator… | ||
| Stream Types | PLDI 2024 | 2024-06-24 |
Proposes a type-theoretic foundation that lets ordinary list programs run as online stream processors by rejecting programs that need unbounded buffering and… | ||
| Getting Productive in Research | PLMW @ ICFP 2023 | 2023-09-04 |
Panel lays out concrete moves: get at least one detailed research letter from someone who knows your work—letters are the most important factor for grad… | ||
| A History of Subtyping | PLMW @ ICFP 2023 | 2023-09-04 |
Traces the technical claim that subtyping is not just a typing convenience but changes computation: adding a subsumption rule breaks the usual… | ||
| Reflecting on Random Generation | ICFP 2023 | 2023-09-04 |
Presents reflective generators that combine free generators + partial monadic profunctors so a generator can run “backwards” to recover random choices that… | ||
| Imagining the Reader | PLMW @ POPL 2023 | 2023-01-17 |
Explains that the hard cause of bad papers is the curse of knowledge and gives concrete fixes: write a concise, falsifiable list of contributions first; assume… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| Testing Differential Privacy with Dual Interpreters | OOPSLA 2020 | 2020-11-15 |
An automated tester called DPCheck converts a common DP proof pattern into a hybrid test that combines instrumented concrete traces and symbolic execution… | ||
| nothing matches | ||