Lars Birkedal
where else to find them
linkedin:lars-birkedal-71b8954b
what they talk about
all 10 in the filters
where they keep going back
all 7 in the filters
on a stage with
all 61 in the filters
who talks about the same things
- Simon Oddershede Gregersen9 talks
- Amin Timany16 talks
- Joseph Tassarotti20 talks
- Alejandro Aguirre10 talks
- Kwing Hei Li6 talks
- Philipp G. Haselwarter6 talks
| title | conference | date |
|---|---|---|
| Cerisier: A Program Logic for Attestation in a Capability Machine | PLDI 2026 | 2026-06-15 |
Cerisier presents a program logic that formalizes CHERI-TrEE support for enclaves on a capability machine and claims modular, end-to-end proofs for systems… | ||
| Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…) | PLDI 2026 | 2026-06-15 |
Claims a program logic that encodes privacy budget as resource inside a probabilistic higher-order separation logic, proves an adequacy theorem linking the… | ||
| Iris-WasmFX: Modular Reasoning for Wasm Stack Switching | PLDI 2026 | 2026-06-15 |
Mechanisation in Rocq produces WasmFXCert and a syntactic type-safety proof for Wasm with explicit stack continuations, proving the extension sound… | ||
| Contextual Refinement of Higher-Order Concurrent Probabilistic Programs | PLDI 2026 | 2026-06-15 |
Claims a new logic, Foxtrot, that proves contextual refinement for higher-order concurrent probabilistic programs and handles higher-order local state… | ||
| Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…) | CPP 2026 | 2026-01-12 |
Defines a reusable distribution typeclass for Eris (Iris-based) that internalizes sampler reasoning, proves a distribution adequacy theorem linking the logical… | ||
| Specifying ABIs with Realizability and Type-Preserving Compilation | PriSC 2026 | 2026-01-11 |
Claims a Realizability model for RichWasm that interprets source types as sets of WebAssembly configurations so a type-preserving compiler yields a memory-safe… | ||
| Reasoning about Weak Isolation Levels in Separation Logic | ICFP 2025 | 2025-10-12 |
Paper formalizes three weak isolation levels for key-value transactions and mechanizes them in Rocq on Iris, giving atomic-style separation-logic specs for… | ||
| Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs | ICFP 2025 | 2025-10-12 |
Presents Coneris, the first higher-order concurrent separation logic that proves numeric error bounds for concurrent probabilistic programs and mechanizes all… | ||
| The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic | CPP 2025 | 2025-01-20 |
Proposes a new modality that permits non-frame-preserving updates to ghost state inside Iris, formalizes a parameterized stack-cutting transformation that… | ||
| Approximate Relational Reasoning for Higher-Order Probabilistic Programs | POPL 2025 | 2025-01-19 |
Describes Approxis, a higher-order separation logic that treats error credits as first-class resources to prove approximate program refinements for an ML-like… | ||
| Modelling Recursion and Probabilistic Choice in Guarded Type Theory | POPL 2025 | 2025-01-19 |
Paper encodes FPC⊕ (recursive types + probabilistic choice) inside clocked guarded type theory and builds operational and denotational semantics connected by a… | ||
| Tachis: Higher-Order Separation Logic with Credits for Expected Costs | OOPSLA 2024 | 2024-10-20 |
Tachis introduces probabilistic cost credits, a separation logic resource that preserves expectation across random branches and lets proofs allocate credits… | ||
| Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…) | OOPSLA 2024 | 2024-10-20 |
Mechanisation produces MSWasmCert as a conservative, proof‑assistant formalisation of MSWasm and WebAssembly 1.0 modules, and builds Iris‑MSWasm: a separation… | ||
| Proving capability safety in the presence of indirect sentries | POCL 2024 | 2024-01-16 |
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces… | ||
| The Essence of Generalized Algebraic Data Types | POPL 2024 | 2024-01-14 |
Presents a minimal core calculus—System Fω+μ with internalized type equalities and injective constant constructors—that directly encodes GADTs, proves… | ||
| The Logical Essence of Well-Bracketed Control Flow | POPL 2024 | 2024-01-14 |
First Hoare-style separation logic for well-bracketed control flow that proves the closure-from-example always returns one when called with a function that… | ||
| Asynchronous Probabilistic Couplings in Higher-Order Separation Logic | POPL 2024 | 2024-01-14 |
Provides a new higher-order relational separation logic called Clutch that proves contextual refinement for a language with impredicative polymorphism… | ||
| Modular Denotational Semantics for Effects with Guarded Interaction Trees | POPL 2024 | 2024-01-14 |
Introduces guarded interaction trees as a denotational domain for higher-order effects, fully formalized in Coq/Iris formalization with reusable artifacts… | ||
| An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T... | POPL 2024 | 2024-01-14 |
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering… | ||
| Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension... | POPL 2024 | 2024-01-14 |
Introduces Trillium as a language-agnostic separation-logic framework that proves intensional refinements between program traces and labeled transition models… | ||
| 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… | ||
| Verifying Reliable Network Components in a Distributed Separation Logic with Dep... | ICFP 2023 | 2023-09-04 |
Claims a verified reliable client–server communication stack implemented in an OCaml-like language (about 300–400 lines of code) that runs over UDP and… | ||
| VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…) | PLDI 2023 | 2023-06-17 |
Formalises a substantial fragment of Arm FF‑A as a toy ISA with hypercalls and develops VMSL separation logic to reason about VM-to-VM shared pages and handoff… | ||
| Iris-Wasm: Robust and Modular Verification of WebAssembly Programs | PLDI 2023 | 2023-06-17 |
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds… | ||
| Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch... | POPL 2023 | 2023-01-15 |
Paper defines operational notions of may- and must-termination as optimal and pessimal termination probabilities, and builds step-indexed logical relations… | ||
| Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed | OOPSLA 2022 | 2022-12-05 |
Introduces directed capabilities that add one extra bit and a single arithmetic bounds check to CHERI-style machines, enabling a calling convention that… | ||
| 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… | ||
| Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr | CPP 2022 | 2022-01-17 |
First formal specification and machine-checked proof of Meta Folly’s fine‑grained MPMC queue: an ML‑style implementation is shown to be a contextual refinement… | ||
| Distributed Causal Memory for Higher-Order Distributed Separation Logic | POPL 2021 | 2021-01-17 |
Presents the first full specification and machine-checked verification of a causally-consistent distributed database implementation and client libraries… | ||
| Efficient, Provable Local Capability Revocation using Uninitialized Capabilities | POPL 2021 | 2021-01-17 |
Proposes uninitialized capabilities that give write-only access to an uninitialized stack region and require overwriting before any read, implemented with… | ||
| Mechanized Logical Relations for Termination-Insensitive Noninterference | POPL 2021 | 2021-01-17 |
Paper proves that a rich information‑flow type system (recursive and existential types, System F impredicative polymorphism, label polymorphism, higher‑order… | ||
| 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 | ||