Robbert Krebbers
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL6 editions2021–2026
- ICFP4 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2026
all 5 in the filters
on a stage with
all 42 in the filters
who talks about the same things
- Derek Dreyer35 talks
- Michael Sammler16 talks
- Jules Jacobs11 talks
- Peter Müller28 talks
- Lars Birkedal35 talks
- Jeehoon Kang14 talks
| title | conference | date |
|---|---|---|
| Backwards-Compatible Row-Based Exceptions in ML | PLDI 2026 | 2026-06-15 |
Type system extends ML with row polymorphism and a new top row to make exception tracking backwards compatible, proving that unannotated code types as top-row… | ||
| Building Blocks for Step-Indexed Program Logics | CPP 2026 | 2026-01-12 |
Claims a single modular physical-step modality lets program-logic designers recover every prior multiple-later elimination technique without redoing… | ||
| 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… | ||
| A Relational Separation Logic for Effect Handlers | POPL 2026 | 2026-01-11 |
Presents blaze, the first mechanised relational separation logic for effect handlers, implemented on Rocq/Iris and proved inside Coq; key idea is a refinement… | ||
| Verified Interpreters for Dynamic Languages with Applications to the Nix Expression(…) | ICFP 2025 | 2025-10-12 |
Paper presents a substitution-based operational semantics using deferred substitutions for dynamic name binding, extends call-by-name lambda calculus to model… | ||
| Affect: An Affine Type and Effect System | POPL 2025 | 2025-01-19 |
Affect introduces Affine types to statically distinguish one-shot versus multi-shot effect continuations, implements a small language called Affect with ML… | ||
| Verified Lock-Free Session Channels with Linking | OOPSLA 2024 | 2024-10-20 |
Claims a verified lock-free implementation of asynchronous, bidirectional session channels (with per-direction buffers and a link/forward operation), proved… | ||
| 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… | ||
| A Proof Recipe for Linearizability in Relaxed Memory Separation Logic | PLDI 2024 | 2024-06-24 |
This work gives a concrete proof recipe and mechanization in Coq (Iris-based iRC11) that reduces manual effort by about 81% via automation, introduces object… | ||
| Unification for Subformula Linking under Quantifiers | CPP 2024 | 2024-01-15 |
Proposes Quantifying on the Uninstantiated, a unification-based algorithm that retroactively turns Evars found during matching into existential quantifiers, so… | ||
| Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O... | POPL 2024 | 2024-01-14 |
LinearActris is a linear concurrent separation logic that claims to give deadlock and leak freedom for message-passing programs by design. The adequacy proof… | ||
| Proof Automation for Linearizability in Separation Logic | OOPSLA 2023 | 2023-10-23 |
Implements proof automation for contextual refinement and logical atomicity inside Diaframe 2.0, encoded in Iris and Coq, and uses both program shape and… | ||
| Dependent Session Protocols in Separation Logic from First Principles | ICFP 2023 | 2023-09-04 |
Three-layer design builds session protocols from mutable references: one-shot channels, then functional session channels, then imperative endpoints; specs use… | ||
| Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic | PLDI 2023 | 2023-06-17 |
Proposes a connection-based multi-succedent calculus that reduces blind backtracking for disjunctive invariants in fine-grained concurrent separation logic… | ||
| CPP Business Meeting | CPP 2023 | 2023-01-16 |
Conference reports concrete numbers: 53 submissions, 25 accepted after a two‑month light double‑blind review with 33 PC members and about 20 external… | ||
| 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… | ||
| 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… | ||
| Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre... | ICFP 2022 | 2022-09-11 |
A functional language MPGV extends GV with multiparty session types, first-class channel endpoints, dynamic spawning and a new redirect construct that enables… | ||
| 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… | ||
| Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L | POPL 2022 | 2022-01-16 |
Introduces connectivity graphs as a generic, parametric graph abstraction plus local Separation Logic predicates that let one prove preservation and global… | ||
| 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… | ||
| Intrinsically Typed Compilation with Nameless Labels | POPL 2021 | 2021-01-17 |
Claims a compositional way to intrinsically type bytecode by replacing global names with nameless labels and a co-contextual interface algebra, implemented as… | ||
| Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S | OOPSLA 2020 | 2020-11-15 |
Derives executable type checkers from Statix specifications by giving an operational semantics that schedules name resolution to avoid unstable queries… | ||
| Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris | ICFP 2020 | 2020-08-23 |
Presents a semantics-first proof that adds guardedness to DOT via a step-indexed logical relation built in Iris, yielding gDOT that models impredicative… | ||
| nothing matches | ||