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
pdf, software, Coq development

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

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

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