Clément Allain
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL2 editions2025–2026
on a stage with
all 8 in the filters
who talks about the same things
- François Pottier14 talks
- Gabriel Scherer12 talks
- Simon Spies8 talks
- Michael Sammler16 talks
- Matthieu Sozeau14 talks
- Alexandre Moine8 talks
| title | conference | date |
|---|---|---|
| Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation(…) | POPL 2026 | 2026-01-11 |
Zoo delivers a transpiler plus proof framework that translates OCaml 5 into a limited ZooLang fragment embedded via a deep embedding in Rocq, where programs… | ||
| Tail Modulo Cons, OCaml, and Relational Separation Logic | POPL 2025 | 2025-01-19 |
Implements Tail Modulo Constructor in the OCaml compiler and shows it reliably turns non‑tail List.map‑style definitions into stack‑safe code; proof of… | ||
| Saturn: a library of verified concurrent data structures for OCaml 5 | OCaml 2024 | 2024-09-07 |
Saturn is an OCaml 5 library on opam providing stack, queue, skiplist, hash table and work‑stealing deque implementations, benchmarked and partly formally… | ||
| Isomorphisms are back! (short talk) | ML 2021 | 2021-08-26 |
A library search tool called dowsing finds functions up to type isomorphism (tuples commutative/associative, unit neutral, currying) and keeps soundness and… | ||
| nothing matches | ||