Homepage of Alban Reynaud Michez, PhD Student in Computer Science.
Contact: alban DOT reynaud AT univ DASH grenoble DASH alpes DOT fr
I am a PhD student in computer science, specifically in the formal study of programming languages. I am working at Verimage laboratory, Grenoble. My supervisors are Sylvain Boulmé and David Monniaux.
LLBC (low-level borrow-calculus) is a model of Rust that is centered around borrows. It was intially introduced for the purpose of the Aeneas verification project. In an ICFP’24 article, Ho, Fromherz and Protzenko studied LLBC. The connected it with an execution model on a heap, specified a borrow-checker (with a symbolic semantics), and proved its soundness.
My PhD project consists in formalizing this work in the Rocq prover. I proved key results about the soundness of LLBC on a minimal fragment, containing mutable borrows, conditionals and loops. This effort lead me to identify a missing argument in the original proof, and to propose a fix. The code is available here. In this preprint we detail the introduced techniques.
With Vincent Rébiscoul, we are working on adding a CompCert backend to this formalization, as a way to have a proof-of-concept certified compiler with a borrow-checker for Rust. This formalization could also serve to prove the soundness of the functional translation of Aeneas.
Modular verification of op-based CRDTs in separation logic
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany and Lars Birkedal, Oopsla 2022.
A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer and Jeremy Yallop, POPL 2021.
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
Ralph Bottesch, Max W. Haslbeck, Alban Reynaud and René Thiemann, NFM 2020.
Formal Verification of Borrow-Checking by Local Commutation Diagram
Alban Reynaud Michez, JFLA 2026.