I am a first-year Ph.D. student in Computer Science within the Cambium team at Inria Paris, in France.

I work under the supervision of Arthur Charguéraud and François Pottier on the formal verification of space bounds, using Separation Logic and space credits.


You can contact me at: firstname.lastname@inria.fr

Otherwise, you can find me in my office at Inria Paris, third floor.

Research interests

I am mainly interested in programming languages and proof theory. At the intersection of the two lives the unicorn I study: the formal proof of programs. The word "proof" refers not only to the proof of functional correctness but also of time bounds, and at the core of my interest, of space bounds.

I am fond of statically typed functional languages, especially OCaml and Haskell. To prove programs correct, I mainly use Coq. Moreover, I am deeply interested in efficient data structures, ranging from chunked se{k,quences} to algebraic graphs.

See my publications and software.