I am a member of the Parsifal team at Inria Saclay - Île de France. I work under the supervision of Dale Miller in the themes of the ERC Advanced Grant ProofCert. I am also part of the Laboratoire d’Informatique at the École polytechnique, where I am a doctoral student and teach under the umbrella of the Université Paris-Saclay.
My research and technical interests revolve around various interrelated topics:
- Proof theory and sequent calculi, proofs and certificates
- Formal specification and verification, proof assistants
- Functional and logic programming, type systems
The grand unifying theme, and pragmatic motivation, is an ambition that I am convinced is both lofty and realistic: this is the need for trust and correctness — in theorems as in the entire pantheon of formalizable artifacts, with software as primus inter pares in today’s world — and a discipline that treats these as first-class abstractions.