Derek Dreyer
where else to find them
what they talk about
all 9 in the filters
where they keep going back
- POPL4 editions2022–2026
- PLDI Workshop Honoring Andreas Podelski4 editions2020–2026
- OOPSLA2 editions2022–2023
all 10 in the filters
on a stage with
all 53 in the filters
who talks about the same things
- Michael Sammler16 talks
- Lennard Gäher7 talks
- Ralf Jung18 talks
- Peter Müller28 talks
- Robbert Krebbers26 talks
- Ranjit Jhala19 talks
| title | conference | date |
|---|---|---|
| VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…) | PLDI 2026 | 2026-06-15 |
Paper proves a machine-checked soundness theorem for a Verus subset by formalizing Verus’s proof-oriented types and translating them into Rust Hornbill–style… | ||
| A Recipe for Modular Verification of Generic Tree Traversals | CPP 2026 | 2026-01-12 |
Presents a concrete verification recipe that models traversal state with a zipper with shadow and characterizes step types as action and silent steps, yielding… | ||
| Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…) | POPL 2026 | 2026-01-11 |
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation… | ||
| JFP Announcement | ICFP 2025 | 2025-10-12 |
Cambridge University Press is dropping the Journal of Functional Programming at end of 2025 and ownership is transferring to the editors with a planned move to… | ||
| Tree Borrows | PLDI 2025 | 2025-06-16 |
Replaces Stacked Borrows’ stack with a per-allocation tree and formalizes aliasing rules so compilers can assume those violations are UB while accepting many… | ||
| Destabilizing Iris | PLDI 2025 | 2025-06-16 |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…) | PLDI 2025 | 2025-06-16 |
Claims a machine‑checked end‑to‑end proof that an interrupt‑free, fixed‑priority, non‑preemptive scheduler meets response‑time bounds by connecting program… | ||
| A Semantic Approach to Robust Property Preservation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so… | ||
| How to Write Papers So People Can Read Them | PLMW @ POPL 2025 | 2025-01-19 |
A concrete checklist of writing moves: state the CGI (context–gap–innovation) trio in the abstract/intro, introduce essential notation just in time, give a… | ||
| Data Race Freedom à la Mode | POPL 2025 | 2025-01-19 |
DRFcaml extends OCaml's type system with new mode axes (contention and portability) to statically guarantee data-race freedom for multi-threaded OCaml while… | ||
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs | PLDI 2024 | 2024-06-24 |
RefinedRust presents a refinement type system that verifies both unsafe Rust and safe Rust by translating MIR into a Coq-embedded Rust model and checking… | ||
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq | PLDI 2024 | 2024-06-24 |
Quiver claims automated inference of full separation logic specs for C code while verifying soundness in Coq using Iris, implemented as a prototype atop… | ||
| Opening | PLMW @ POPL 2024 | 2024-01-17 |
Conference includes 93 papers from 319 submissions, nine distinguished papers, two invited talks (Azay Farzon and Nate Foster), and session previews… | ||
| Later Credits: A Case Study in the Unreasonable Effectiveness of Separation ... | O'Hearn Fest (POPL 2024) | 2024-01-14 |
Presents a concrete mechanism inside Iris that turns the later modality into an ownable resource called later credits, letting a step produce a credit and… | ||
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C | OOPSLA 2023 | 2023-10-23 |
Melocoton claims the first formal semantics of the OCaml FFI and the first multi‑language program logic that reasons about OCaml and C interactions… | ||
| Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasonin... | OOPSLA 2023 | 2023-10-23 |
Outcome Logic (OL) replaces a single postcondition with outcome-indexed assertions over sets of states, adds an outcome conjunction that composes reachable… | ||
| Stuttering for Free | OOPSLA 2023 | 2023-10-23 |
Presents FreeSim, a new stuttering-simulation technique mechanized in Coq that replaces the usual “synchronous progress” requirement with asynchronous… | ||
| Conditional Contextual Refinement | POPL 2023 | 2023-01-15 |
A new refinement notion, Conditional Contextual Refinement (CCR), combines separation-logic pre/post conditions with transitive contextual refinement by… | ||
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification | POPL 2023 | 2023-01-15 |
DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a… | ||
| 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… | ||
| Finding real bugs in big programs with incorrectness logic | OOPSLA 2022 | 2022-12-05 |
Pulse-X applies ISL (a synthesis of Incorrectness Logic and separation logic) to build an automatic under-approximate analyzer for memory errors, inferring… | ||
| Proving Hypersafety Compositionally | OOPSLA 2022 | 2022-12-05 |
Claims a new proof system, the Logic for Hyper-triple Composition (LHC), that proves hypersafety properties compositionally by treating mixed-arity… | ||
| BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs | OOPSLA 2022 | 2022-12-05 |
A foundational, automated verifier encodes common bitfield patterns as structured bit vectors and implements partial, semantics-preserving operations (masking… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | ICFP 2022 | 2022-09-11 |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| VIP: Verifying Real-World C Idioms with Integer-Pointer Casts | POPL 2022 | 2022-01-16 |
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying… | ||
| Concurrent Incorrectness Separation Logic | POPL 2022 | 2022-01-16 |
Develops CISL as a parametric extension of Incorrectness Separation Logic that models concurrency with histories and lock-aware events, instantiates to race… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| How To Write Papers So People Can Read Them | PLMW @ ICFP 2020 | 2020-08-23 |
Presents a set of concrete, testable rules for readable papers: enforce sentence flow with old-to-new beginnings and endings, guarantee coherence with one… | ||
| Ask Me Anything with Felix Klock | PLDI 2020 | 2020-06-15 |
A live Q&A at PLDI 2020 explains concrete Rust work: ongoing unsafe code guidelines to write down rules, a dynamic checker implemented in the Miri interpreter… | ||
| How To Write Papers So People Can Read Them | SPLASH 2019 PLMW | 2019-10-20 |
Prescribes concrete, checkable rules: start sentences with old to new information and give each paragraph one paragraph one point so readers never lose the… | ||
| nothing matches | ||