I am a PhD student in computer science at the Laboratoire Méthodes Formelles (LMF) under the supervision of Frédéric Blanqui and Patrick Massot.

Currently, I work in translating (and aligning) the standard library of HOL Light to Lean4. slides

I’m also interested in the development of Proof Assistants (mostly Lean), its use for education and formalization of mathematics.

Teaching

I teach C++ at the IUT Orsay.

Publications

Nothing here (yet).