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

Tail Modulo Cons, OCaml, and Relational Separation Logic
POPL 2025
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
preprint, Coq development

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

Drafts

Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic
Clément Allain
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