Currently, I am a postdoctoral researcher in the Formally Verified Security group (FOVSEC) at the Max Planck Institute for Security and Privacy (MPI-SP) (previously a Starting Researcher in the Prosecco team at Inria Paris). I work with Cătălin Hriţcu, previously as part of 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:

• Programming languages: proof assistants; formal specification, testing and verification; proof certificates; type systems; computational logic.

• Computer security: secure compilation; compartmentalization; security policies; hardware enforcement; micropolicies; capability machines.

The principal objective of my work at FOVSEC 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 (now Partout) at the LIX laboratory at École polytechnique in Université Paris-Saclay, and Inria Saclay - Île de France. I was advised by Dale Miller working in the ERC ProofCert project.

A grand unifying theme and pragmatic motivation of my research is an ambition that I am convinced is both lofty and realistic: this is the need for trust (which encompasses a notion of security) 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.