Currently, I am a Starting Researcher in the Prosecco team at Inria of Paris. I work with Cătălin Hriţcu in the ERC SECOMP project and the DARPA SSITH HOPE project.

My research interests are centered around the development and application of formal methods to solve computer security problems, developed along both axes:

The principal objective of my work at Prosecco is to build secure compilation chains that preserve useful classes of security properties while scaling to realistic programming languages and enabling efficient and secure program execution.

Previously, I was a doctoral researcher in the Parsifal team at the LIX laboratory at École polytechnique and Inria Saclay - Île de France. I was advised by Dale Miller working in the ERC ProofCert project.

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.