Maxime Legoupil
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2026
all 4 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Jean Pichon-Pharabod12 talks
- Aina Linn Georges12 talks
- June Rousseau2 talks
- Conrad Watt12 talks
- Philippa Gardner17 talks
- Xiaojia Rao3 talks
| title | conference | date |
|---|---|---|
| Iris-WasmFX: Modular Reasoning for Wasm Stack Switching | PLDI 2026 | 2026-06-15 |
Mechanisation in Rocq produces WasmFXCert and a syntactic type-safety proof for Wasm with explicit stack continuations, proving the extension sound… | ||
| Specifying ABIs with Realizability and Type-Preserving Compilation | PriSC 2026 | 2026-01-11 |
Claims a Realizability model for RichWasm that interprets source types as sets of WebAssembly configurations so a type-preserving compiler yields a memory-safe… | ||
| Iris-Wasm: reasoning formally about Wasm and Wasm extensions | WebAssembly Workshop @ ICFP/SPLASH 2025 | 2025-10-16 |
Iris-Wasm is a Coq mechanisation of WebAssembly 1.0 built on the Iris framework that gives a higher-order, modular separation logic and a machine-checked… | ||
| Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…) | OOPSLA 2024 | 2024-10-20 |
Mechanisation produces MSWasmCert as a conservative, proof‑assistant formalisation of MSWasm and WebAssembly 1.0 modules, and builds Iris‑MSWasm: a separation… | ||
| Iris-Wasm: Robust and Modular Verification of WebAssembly Programs | PLDI 2023 | 2023-06-17 |
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds… | ||
| nothing matches | ||