Armaël Guéneau


portrait Starting from January 1st, 2022, I will be a researcher at Inria Saclay in the Toccata team!
I am currently a post-doc at Aarhus University, working with Lars Birkedal since January 2020.
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.

I am currently part of an exciting project on 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.

Research interests

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.