Room 206 (2nd floor, badged access)
26 November 2026 - 14h00
Proxy-based small inversions for the Rocq prover
by Basile Gros from Université Grenoble Alpes
invited by Jean-François MONIN
26 November 2026 - 14h00
Proxy-based small inversions for the Rocq prover
by Basile Gros from Université Grenoble Alpes
invited by Jean-François MONIN
Abstract: Rocq is an interactive proof assistant that was developed at Inria and other institutions, and is well recognized (ACM award). In the field of proof of correctness of software, it is used in many substantial projects such as the CompCert certified compiler (also ACM award).
The internal language of Rocq is based on the notion of inductive construction which is used to define, on the one hand, algebraic types to represent the objects on which we reason and, on the other hand, the logical relations which express the properties of these objects, and the functions using those algebraic types. Inversion is a reasoning scheme frequently used to simplify case-analysis by eliminating, a priori, many situations that are absurd by construction. For instance, inversion steps occur very frequently in proofs about the semantics of the programs compiled by CompCert, and to define function in the scope of dependent programming.
The current implementations of this inversion technique in Rocq chose to cover as many cases as possible by using complex reasoning and algorithms, with the drawback of a greater complexity in the body of the proofs and functions defined with them.
This PhD thesis describes an alternative approach to inversion, called 'proxy-based small inversions', that were initially developed by Jean-François Monin and that promote a more transparent version of this kind of reasoning. The results described in this thesis are on the one hand a systematic theoretical description of this approach, and on the other hand an implementation of an automated procedure to generate the intermediate definitions that proxy-based small inversions rely on.
