I am a permanent researcher in the Toccata team at Inria Saclay.
I was previously a post-doc at Aarhus University, working with Lars Birkedal in 2020-2021.
Before that, I completed my PhD in the Gallium team at Inria from 2016 to 2019, working with Arthur Charguéraud and François Pottier.
The topic of my PhD thesis is the formalization of asymptotic complexity properties of programs, using the CFML Coq library.
During my post-doc I was part of an exciting project formalizing high-level
security properties for low-level code running on
CHERI-like capability machines, using the
Iris framework. For a gentle introduction to our
methodology for reasoning formally about programs interacting with untrusted
code on capability machines, see our journal draft
paper (currently submitted for publication).
All our results are formalized in Coq+Iris, and available online: see cerise and cerise-stack.
My interests include formal proofs of programs and functional programming. I enjoy figuring out why complex code actually works and formalizing why it does indeed so; but I also like the process of building better abstractions to manage software complexity.
Most of my work involves a proof assistant (typically Coq), or a statically typed programming language such as OCaml. I am generally curious about language implementation techniques, and the use of OCaml as a systems' programming language. I also have a sweet spot for automated decision procedures, in particular as a well-behaved helping hand for interactive mechanized proofs.
Check out my publications and software.
Arm-a-el Gue[as in guest]-no