Emanuele D'Osualdo
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2022–2026
on a stage with
all 19 in the filters
who talks about the same things
- Kengo Hirata5 talks
- Michael Sammler16 talks
- Michael Carbin14 talks
- Simon Spies8 talks
- Oded Padon11 talks
- Yusuke Matsushita7 talks
| title | conference | date |
|---|---|---|
| RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing | POPL 2026 | 2026-01-11 |
RapunSL presents a program logic that adds linear combination (scalar multiply and plus) and a separate mixing connective to quantum separation logic, so… | ||
| Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning | POPL 2025 | 2025-01-19 |
Bluebell is a program logic that unifies unary and relational proofs by adding a joint conditioning modality that encodes conditional independence and… | ||
| 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… | ||
| The Path to Durable Linearizability | POPL 2023 | 2023-01-15 |
Proposes a concrete method that converts an existing linearizability proof into durable correctness by adding small, checkable Delta proof obligations that… | ||
| 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… | ||
| A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in | OOPSLA 2022 | 2022-12-05 |
A session-typed π-calculus extracted from the Logic of Bunched Implications, called πBI, implements a new runtime spawn primitive that duplicates providers… | ||
| TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr | POPL 2022 | 2022-01-16 |
TaDA Live claims compositional proofs of termination for blocking fine‑grained concurrent programs by extending separation logic with a semantic model of… | ||
| nothing matches | ||