Leo Stefanesco
where else to find them
what they talk about
where they keep going back
- POPL2 editions2022–2024
on a stage with
all 23 in the filters
who talks about the same things
- Amin Timany16 talks
- Siddharth Bhat4 talks
- Lars Birkedal35 talks
- Thomas Reps20 talks
- Michael Sammler16 talks
- Tobias Grosser14 talks
| title | conference | date |
|---|---|---|
| Interactive Bit Vector Reasoning using Verified Bitblasting | OOPSLA 2025 | 2025-10-16 |
A verified bit-blasting pipeline called bv_decide tactic compiles Lean bitvector goals to AIGs, converts to CNF, calls an external SAT solver that emits… | ||
| Certified Decision Procedures for Width-Independent Bitvector Predicates | OOPSLA 2025 | 2025-10-16 |
Mechanized, executable decision procedures in Lean for width-independent bitvectors that formalize k-induction, automata reachability, emptiness checking and… | ||
| 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… | ||
| Layered and Object-Based Game Semantics | POPL 2022 | 2022-01-16 |
Presents a concrete game-semantics model where a layer interface is an object type plus an object strategy, implementations are regular maps from underlay to… | ||
| 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 | ||