Paolo G. Giarrusso
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 6 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Aggelos Biboudis3 talks
- Fengyun Liu4 talks
- Ondřej Lhoták11 talks
- Leo Stefanesco6 talks
- Jonathan Aldrich17 talks
- Ugo Dal Lago14 talks
| title | conference | date |
|---|---|---|
| Recursive Mutexes in Separation Logic | RocqPL 2026 | 2026-01-17 |
Develops a separation-logic specification for recursive mutex built on the Brick logic and derived from a lower-level logically-atomic spec, with a per-thread… | ||
| Modularizing CPU Semantics for Virtualization | PriSC 2024 | 2024-01-20 |
Proposes a concrete decomposition of ARM ASL into an unprivileged core and a small privileged handler so one common unprivileged semantics can be reused across… | ||
| A Case for Lightweight Interfaces in Coq | CoqPL 2022 | 2022-01-22 |
Bedrock uses Coq and the Iris program logic to verify a large concurrent C++ hypervisor stack and finds Coq’s lack of lightweight interface files hurts scale… | ||
| A Type-and-Effect System for Object Initialization | OOPSLA 2020 | 2020-11-15 |
Type-and-effect design enforces a concretely checkable initialization discipline: cold, warm, hot types plus potentials and effects track field accesses… | ||
| 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… | ||
| The DOT Calculus: An Introduction for Scala Programmers | Scala World 2019 | 2019-09-11 |
Small core calculus formalizes the Scala 3-ish type system and claims type soundness with fully mechanized proofs verifying that well-typed programs do not get… | ||
| nothing matches | ||