Welcome!
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.
Contact: firstname.lastname@inria.fr
(github | mastodon | IRC)
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.
Current projects:
- My current research project is Melocoton. In Melocoton, we tackle verified cross-language interoperability, looking in particular at the OCaml/C foreign function interface. The goal is: given C code that uses the OCaml FFI, formally verify that it is safe to link with the OCaml runtime, and satisfies a functional correctness specification that can be exploited from OCaml code. See in particular our OOPSLA'23 paper.
- I am part of the Gospel research project trying to develop a useful and developer-friendly formal specification language for OCaml.
Other cool topics I have worked on in the past:
- Formalizing high-level security properties for low-level code running on CHERI-like capability machines (during my post-doc). For a gentle introduction to our methodology for reasoning about untrusted code on capability machines, see our journal draft paper and coq development.
- Formalization of asymptotic complexity bounds as well as functional correctness for OCaml programs (during my PhD).
- Adding a Separation Logic framework to CakeML for verifying the functional correctness of effectful programs.
Tools and techniques
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.
PhD students
- Arnaud Golfouse (2023-) (co-advised by Jacques-Henri Jourdan and myself)
Dossier de candidature CR Inria/CNRS
À des fins de transparence, mes dossiers de candidatures à des postes de chargé de recherche. (J'ai candidaté début 2021, été auditionné au CNRS et à l'Inria, et finalement recruté cette année là par l'Inria dans l'équipe Toccata).
- CNRS: rapport d'activité, projet de recherche, transparents
- Inria: dossier (équipe Celtique), dossier (équipe Toccata) , transparents (Celtique), transparents (Toccata)
How to pronounce my name
Arm-a-el Gue[as in guest]-no
In IPA: /aʁmaɛl geno/