Clément Allain

(fun x y -> x^"."^y^"@inria.fr") "clement" "allain"

github

Hi! I am a third year Ph.D. student in computer science at INRIA Paris. My advisor is Gabriel Scherer.

I am mainly interested in mechanized formal verification, including program verification using the Iris separation logic and verified compilation.

Publications

Saturn: a library of verified concurrent data structures for OCaml 5
OCaml Workshop 2024
Clément Allain, Vesa Karvonen, Carine Morel

Snapshottable stores
ICFP 2024, Distinguished Paper Award
Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer

Correct tout seul, sûr à plusieurs
JFLA 2024
Clément Allain, Gabriel Scherer

Talks

Verifying Tail Modulo Cons using Relational Separation Logic
Iris Workshop 2024

Correct tout seul, sûr à plusieurs
JFLA 2024

Verification of Chase-Lev work-stealing deque
Iris Workshop 2023

Teaching

2023-2024 Functional programming (OCaml)
2023 Introduction to operating systems