Amphi E à l'Ensimag (près de l'IM2AG)
26 November 2026 - 14h00
Proxy-based small inversions for the Rocq prover (Phd Defense)
by Basile Gros from Université Grenoble Alpes
26 November 2026 - 14h00
Proxy-based small inversions for the Rocq prover (Phd Defense)
by Basile Gros from Université Grenoble Alpes
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.
Jury:
- Hugo Herbelin (Rapporteur)
- Guillaume Melquiond (Rapporteur)
- Assia Mahboubi
- Catherine Dubois
- Dominique Larchey-Wendling
- Matthieu Sozeau
- Alain Girault
