Armaël Guéneau


portrait 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. See our POPL'21 paper, and also a more tutorial-like presentation of some of our methodology, in a simpler, more approachable setting. (An extended version is currently being worked on, stay tuned!)

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.