Room 206 (2nd floor, badged access)
22 January 2026 - 14h00
Formal Verification of Borrow-Checking by Local Commutation Diagrams
by Alban Reynaud from Verimag
invited by Sylvain BOULME
22 January 2026 - 14h00
Formal Verification of Borrow-Checking by Local Commutation Diagrams
by Alban Reynaud from Verimag
invited by Sylvain BOULME
Abstract: The Rust programming language provides a safe alternative to C and C++ for system programming. In particular, it achieves memory safety with an ownership-based typing discipline, providing a notion of borrows as a restriction on aliasable pointers. The discipline of borrows is statically enforced by a component of the compiler called the borrow-checker.
In their article published at the ICFP conference in 2024, Ho, Fromherz and Protzenko prove that LLBC, a borrow-centric model of Rust, can be equipped with a symbolic semantics that plays the role of a borrow-checker. They also prove that LLBC is a sound model with respect to an operational semantics over a standard memory model a la CompCert.
We initiate the formalization of this work in the Rocq proof assistant. In particular, we found a flaw in the proofs of some of their fundamental lemmas. We repair their methodology using techniques from rewriting theory. We finally present the current state of our formalization, and how we use a rewriting system to automate proofs.
Rehearsal of the talk at JFLA'26 the following week. The JFLA paper and the slides are in English. But the talk will be given in French (JFLA = French conference).
