Room 206 (2nd floor, badged access)
26 novembre 2026 - 14h00
Petites inversions par proxy pour Rocq
par Basile Gros de Université Grenoble Alpes
invité(e) par Jean-François MONIN
26 novembre 2026 - 14h00
Petites inversions par proxy pour Rocq
par Basile Gros de Université Grenoble Alpes
invité(e) par Jean-François MONIN
Résumé : Rocq est un assistant interactif à la preuve développé à l'Inria et dans d'autres laboratoires, et qui fait autorité (prix ACM). Dans le domaine de la preuve de correction de logiciels, il est utilisé dans de nombreux projets parfois très conséquents comme le compilateur certifié CompCert (prix ACM également).
Le langage interne de Rocq repose sur la notion de construction inductive qui sert à définir d'une part des types algébriques pour représenter les objets sur lesquels on raisonne et d'autre part des relations logiques qui expriment les propriétés de ces objets ou des fonctions qui reposent sur des types algébriques. L'inversion est un schéma de raisonnement fréquemment utilisé pour simplifier les raisonnements par cas en éliminant a priori des situations impossibles par construction. L'inversion est notamment très présente dans les preuves sur la sémantique des programmes compilés par CompCert, et dans la programmation avec types dépendants.
Les implémentations actuelles de l'inversion en Rocq choisissent de couvrir le plus de cas possible en utilisant une machinerie et des raisonnements complexes au prix d'une grande complexité dans le corps des prédicats et fonctions ainsi définis.
Cette thèse décrit une approche différente à l'inversion, plus 'légère' dite 'petites inversions par proxy', initialement développées par Jean-François Monin, qui promeut une version plus transparente de ce type de raisonnement. Les résultats de cette thèse sont une description théorique systématique de cette approche, ainsi que l'implémentation d'une procédure automatisée de génération des définitions intermédiaires utilisées par ces petites inversions.
