I’m a postdoc at the Max Planck
Institute for Security and Privacy, in the Foundations of Security
and Privacy group lead by Gilles
Barthe.
Before that, I was a PhD student in the Toccata Inria team from the LMF laboratory (Paris-Saclay
University) under the supervision of Guillaume Melquiond.
Research
I’m interested in programming languages, compilation and formal
proofs.
During my PhD, I worked on Capla, a
programming language dedicated to writing low-level computer algebra
libraries (e.g., GMP, BLAS, FFTW). This language is designed to be safe
and to ease deductive program verification, while being low-level enough
to be suitable for this kind of computationally intensive applications.
I also developed a compiler for this language. It uses the CompCert formally verified compiler as
a backend. The semantics of Capla, as well as the proofs of safety and
compiler correctness, have been formalized with the Rocq Prover.
Publications
- Programming language and formally verified compiler for low-level
numerical libraries (HAL, PDF) 2025
PhD Thesis
Slides (PDF)
- Des briques de calcul formel plus solides avec Capla (HAL, PDF)
2025
36es Journées Francophones des Langages
Applicatifs (JFLA 2025)
- A Safe Low-Level Language for Computer Algebra and Its Formally
Verified Compiler (HAL, PDF,
DOI, Artifact) 2024
29th ACM SIGPLAN International Conference
on Functional Programming (ICFP 2024)
- Jonglerie Musicale : Quand les notes de musiques subissent la
gravité (HAL, PDF)
2023
Pousses de chercheurs & chercheuses, édition
n°1
- Les nombres premiers au crible de la preuve formelle (HAL, PDF) 2021
32es Journées Francophones des Langages
Applicatifs (JFLA 2021)
Teaching
- Langages, interprétation, compilation (LDD3 Info-Maths, 48h)
- Algorithmique (L3 Info, 42h)
- Programmation fonctionnelle avancée (L3 Info, 24h)
- Architecture des ordinateurs (L2 Info, 24h)
- Bases de données (L2 Info, 24h)
- Programmation objet et génie logiciel (L2 Info, 24h)
