Home

News

Conditionally accepted at ICFP'24: "A Two-Phase Infinite/Finite Low-Level Memory Model".
Joint work with Calvin Beck, Irene Yoon, Hanxi Chen and Steve Zdancewic

Conditionally accepted at ICFP'24: "Abstract Interpreters: a Monadic Approach to Modular Verification".
Joint work with Sébastien Michelland and Laure Gonnord.

New draft available: "A concurrency model based on monadic interpreters -- Executable semantics for a concurrent subset of LLVM IR".
Joint work with Nicolas Chappe and Ludovic Henrio.

New draft available: "An abstract, certified account of operational game semantics".
Joint work with Peio Borthelle, Tom Hirschowitz and Guilhem Jaber.

Galaad Langlois has presented his work on formalizing W-types and M-types axiom free in Coq at the Coq Workshop 2023!
Joint work with Galaad Langlois and Damien Pous.

Students

I have the great pleasure to co-advise two brilliant PhD students:

Nicolas Chappe (co-advised with Ludovic Henrio)
Peio Borthelle (co-advised with Tom Hirschowitz and Guilhem Jaber)