Formalisation of the Bigraph Theory in the Rocq proof assistant

La théorie des bigraphes de Robin Milner a été utilisée aussi bien pour représenter des modèles de calcul que comme outil de modélisation. Elle constitue un modèle mathématique pour les systèmes ubiquitaires ayant deux dimensions complémentaires: l'agencement spatial et hiérarchique des composants, ainsi que les connexions entre ces composants. Les bigraphes connaissent des applications dans de nombreux domaines de la biologie jusqu'aux jeux à réalité mixte.Un bigraphe est une structure comprenant deux graphes, basés sur un même ensemble de nœuds, représentant chacun une dimensions : un graphe de liens pour les connexions entre les nœuds, et un graphe de lieux pour la position et la hiérarchie des différents nœuds. Les bigraphes modélisent également les aspects dynamiques de ces systèmes au travers de règles de réaction : le mouvement des composants et leurs inter-connexions. Un bigraphe muni de règles de réactions constitue un système réactif bigraphique (BRS) qui modélise donc un système et son évolution. Les bigraphes sont conçus pour être combinés et emboîtés, de sorte que des systèmes complexes puissent être construits de manière systématique à partir de composants plus simples, grâce à des opérateurs permettant d'assembler deux bigraphes entre eux.Dans des travaux récents, les bigraphes ont été utilisés pour modéliser la sémantique formelle d’un langage de description d’interfaces homme-machine, BIGUIL. Ce langage permet ainsi de représenter des systèmes interactifs par des BRS. Nous cherchons à traduire des propriétés sur ces systèmes en propriétés sur le modèle mathématique, et nous intéressons à la vérification de ces propriétés.Pour vérifier des propriétés sur BIGUIL et sur des programmes en BIGUIL, la littérature fournit de multiples implémentations des bigraphes, mais aucune dans un environnement pouvant fournir les garanties d'une formalisation dans un assistant de preuves. Plus généralement, il n'existe pas non plus de formalisation de la théorie des bigraphes dans ces environnements.Les assistants de preuves comme Rocq (anciennement Coq), Isabelle ou Lean permettent à la fois de modéliser précisément des systèmes et de construire des preuves de propriétés sur ces systèmes vérifiées informatiquement. Ils permettent la vérification d'artefacts dont la complexité dépasse la portée du raisonnement automatisé seul ou du “papier et crayon” seul. Ainsi, la formalisation de modèles mathématiques en Rocq est d'un intérêt certain pour la communauté : cela permet à la fois de vérifier la bonne définition du modèle, mais aussi de fournir un environnement dans lequel raisonner formellement et de façon vérifiée sur des systèmes modélisés par ces sémantiques.Ainsi, dans cette thèse nous présentons BiCoq: une implémentation entièrement formelle de la théorie des bigraphes de Robin Milner dans l’assistant de preuves Rocq. Nous définissons le type des bigraphes abstraits ainsi que les outils classiques qui peuvent être attendus pour construire des bigraphes : les deux notions principales d'équivalence et les opérateurs de produit tensoriel, composition, produit parallèle, produit de fusion (merge product) et l'imbrication (nesting). Nous nous appuyons pour cela sur les types dépendants de Rocq, ainsi que sur les typeclass pour représenter les conditions d’application d’opérateurs partiels sur les bigraphes. Nous démontrons rigoureusement la correction de ces opérateurs, et nous prouvons que notre formalisation vérifie les axiomes énoncés par Milner sur la catégorie des bigraphes abstraits (catégorie symétrique, partielle et monoïdale).