Jean Pichon-Pharabod
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2026
all 8 in the filters
on a stage with
all 21 in the filters
who talks about the same things
- Maxime Legoupil5 talks
- Aina Linn Georges12 talks
- Conrad Watt12 talks
- June Rousseau2 talks
- Philippa Gardner17 talks
- Bryan Parno22 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… | ||
| What is Fairy Dust? Universal Contracts for WebAssembly | WebAssembly Workshop @ ICFP/SPLASH 2025 | 2025-10-16 |
Proposes making WebAssembly’s informal “fairy dust” into explicit universal contracts by identifying, formalizing and proving language guarantees such as type… | ||
| Synchronous Programming for Kids: A Manifesto | Onward! 2025 | 2025-10-12 |
Argues that primary‑school game programming fits a synchronous model better than Scratch’s imperative handlers and shows a working prototype called Reactive… | ||
| CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq | CPP 2025 | 2025-01-20 |
A verified backend implemented and proven in Coq generates WebAssembly modules from CertiCoq’s Lambda ANF, mechanised against WasmCert-Coq and offering a… | ||
| 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… | ||
| CertiCoq-Wasm: Verified compilation from Coq to WebAssembly | CoqPL 2024 | 2024-01-20 |
A verified compiler from Gallina (Coq) to WebAssembly is implemented and mechanised against the WasmCert-Coq formalisation, reusing the CertiCoq pipeline and… | ||
| Proving capability safety in the presence of indirect sentries | POCL 2024 | 2024-01-16 |
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces… | ||
| An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T... | POPL 2024 | 2024-01-14 |
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering… | ||
| VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…) | PLDI 2023 | 2023-06-17 |
Formalises a substantial fragment of Arm FF‑A as a toy ISA with hypercalls and develops VMSL separation logic to reason about VM-to-VM shared pages and handoff… | ||
| 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 | ||