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.
(github | mastodon | IRC)
→ Stages 2022-2023 : je recherche des stagiaires ! Voir mes sujets de stage.
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.
Other cool topics I have worked on in the past:
Most of my work involves a proof assistant (typically Coq), and a statically typed programming language such as OCaml. I am most used to program logics as a way to reason about programs; Separation Logic is my bread and butter. In particular, these days I am a user of the Iris Separation Logic framework.
I am generally curious about language implementation techniques, compilers, 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