I am a PhD student in computer science at the Laboratoire Méthodes formelles (LMF), on the subject of translating Isabelle proofs to Rocq (or Lean), supervised by Frédéric Blanqui.

News

• Here is the link to this semester’s Logic Project course

Presentations

• I presented work from my 2025 internship online at the Rocqshop 2025
  Presentation subject: “Automating alignments of HOL Light inductive types and recursive functions in Rocq”
  Here are the slides and the recording.

Education

• 2018-2021 Licence Parcours Spécial Mathématiques (Université Paul Sabatier, Toulouse)
  Special Course Bachelor’s in Mathematics

• 2021-2023 Master Logique Mathématiques et Fondements de l’Informatique (LMFI) (Université Paris Cité, Paris)
  Master’s in Mathematical Logic and Foundations of Computer Science

• 2023-2024 Préparation à l’Agrégation externe de Mathématiques (Université Paris Cité, Paris)
  Preperation to the mathematics Agrégation, french national exam for secondary school teachers

Teaching

• 2024-2025 Spent three months as an intern mathematics teacher at the Lycée de Villaroy in Guyancourt at the start of the scholar year
  (classes for 2de GT and Tle STMG)
• 2025-2026
  • S1 exercise sessions of the rewriting course of the M1 MPR1 at ENS Paris Saclay
  • S2 Logic Project of the L3 Computer Science of ENS Paris Saclay with Raphaël Berthon

Curriculum Vitae

my CV (in french)