| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Wed, 17 Dec 2025 21:51:40 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"694325ec-1a58"
expires: Sun, 28 Dec 2025 07:37:16 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: E050:2916CC:7660EF:848F97:6950DBD4
accept-ranges: bytes
age: 0
date: Sun, 28 Dec 2025 07:27:16 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210096-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1766906836.082910,VS0,VE219
vary: Accept-Encoding
x-fastly-request-id: 0c5613daa8c71feb87417229a88d3b8a1b73686e
content-length: 1596
Clément Allain
Clément Allain
(fun x y -> x^"."^y^"@inria.fr") "clement" "allain"
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
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
Drafts
PhD thesis
Talks
Iris Workshop 2025
Cambium seminar (2025/03/21)
JFLA 2025
POPL 2025
Iris Workshop 2024
JFLA 2024
Iris Workshop 2023
Teaching
| Summer 2025 | Functional programming (OCaml) |
| Fall 2024 | |
| Summer 2024 | |
| Fall 2023 | |
| Fall 2023 | Introduction to operating systems |