Arthur Charguéraud
where else to find them
what they talk about
where they keep going back
- POPL2 editions2023–2026
all 5 in the filters
on a stage with
all 7 in the filters
who talks about the same things
- Alexandre Moine8 talks
- François Pottier14 talks
- Jean-Marie Madiot2 talks
- Jeehoon Kang14 talks
- Michael Sammler16 talks
- Peter Müller28 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… | ||
| A Core Language for Extended Pattern Matching and Binding Boolean Expressions | ML 2025 | 2025-11-24 |
Presents a small core language that encodes guarded patterns, active/view deconstructors, and Rust-style if-let chains by treating pattern tests as binding… | ||
| Interactive Source-to-Source Optimizations Validated using Static Resource Analysis | SOAP 2024 | 2024-06-25 |
OptiTrust is an interactive source-to-source optimizer for C that uses a lightweight Separation-Logic-based static resource analysis to verify each… | ||
| 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… | ||
| Separation Logic for Sequential Programs (Functional Pearl) | ICFP 2020 | 2020-08-23 |
A mechanized formalization claims a teachable Separation Logic for sequential programs with all definitions and proofs encoded in Coq formalization and… | ||
| nothing matches | ||