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; secure hardware.
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.