Alexandre Moine
where else to find them
linkedin:alexandre-moine-21b3bb205
what they talk about
where they keep going back
- POPL3 editions2023–2026
on a stage with
all 9 in the filters
who talks about the same things
- Arthur Charguéraud7 talks
- François Pottier14 talks
- Sam Westrick12 talks
- Jean-Marie Madiot2 talks
- Michael Sammler16 talks
- Amin Timany16 talks
| title | conference | date |
|---|---|---|
| Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage(…) | POPL 2026 | 2026-01-11 |
IrisFit is a separation logic, formalized in Coq on top of the Iris framework, that uses space credits to bound heap usage for a concurrent call-by-value… | ||
| TypeDis: A Type System for Disentanglement | POPL 2026 | 2026-01-11 |
TypeDis is a type system that guarantees any well-typed program is disentangled and so permits task-local, synchronization-free garbage collection; it… | ||
| All for One and One for All: Program Logics for Exploiting Internal Determinism in(…) | POPL 2026 | 2026-01-11 |
Defines schedule-independent safety: showing one terminating execution is safe suffices to guarantee safety for all schedules. Introduces separation logic… | ||
| PLMW Panel | PLMW @ POPL 2025 | 2025-01-19 |
Career-panelists compare concrete career moves and tactics: experiences range from working at an employee‑owned consultancy with ~110 engineers to junior… | ||
| DisLog: A Separation Logic for Disentanglement | POPL 2024 | 2024-01-14 |
Claims a first static program logic that proves disentanglement for fork‑join programs and gives a high‑level variant that yields disentanglement for race‑free… | ||
| A High-Level Separation Logic for Heap Space under Garbage Collection | POPL 2023 | 2023-01-15 |
Logic gives a concrete way to prove heap-space bounds under a GC that follows the free-variable rule: allocation consumes space credits, deallocation returns… | ||
| Specification and Verification of a Transient Stack | CPP 2022 | 2022-01-17 |
Defines and machine-verified a scaled-down transient stack implemented as a list of fixed-capacity chunks with unique identifiers for ownership, copy‑on‑write… | ||
| nothing matches | ||