Clément Allain

Hi! I'm a postdoctoral researcher in the Logic and Semantics group at Aarhus University, working on CHERI-like capability machines with Lars Birkedal, Jean Pichon-Pharabod and June Rousseau.

Before that, I was a Ph.D. student at INRIA Paris. My advisors were François Pottier and Gabriel Scherer.

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

Publications

Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic

POPL 2026

Clément Allain, Gabriel Scherer

Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic

JFLA 2025

Clément Allain

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

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

Summer 2025	Functional programming (OCaml)
Fall 2024
Summer 2024
Fall 2023
Fall 2023	Introduction to operating systems