Jacques-Henri Jourdan
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 4 in the filters
who talks about the same things
- Glen Mével2 talks
- François Pottier14 talks
- Jules Jacobs11 talks
- Armaël Guéneau7 talks
- Simon Spies8 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust | CPP 2026 | 2026-01-12 |
Creusot gains support for linear ghost resources and implements a ptr_own with permission map that lets mutable borrows be expressed and borrow‑checked in… | ||
| Thunks and Debits in Separation Logic with Time Credits | POPL 2024 | 2024-01-14 |
Machine‑checked reconstruction of Okasaki’s debit reasoning implemented in Iris$, with proofs and reusable artifacts (Zenodo/GitLab). Formalizes the missing… | ||
| Cosmo: A Concurrent Separation Logic for Multicore Ocaml | ICFP 2020 | 2020-08-23 |
Cosmo provides a separation logic for Multicore OCaml that exposes the weak memory model yet lets you verify familiar locks: it instantiates Iris and is… | ||
| nothing matches | ||