Description du sujet de thèse

Contexte de la thèse

L'avènement récent de la théorie des catégories appliquée et les projets de formalisation des mathématiques à grande échelle à l'aide d'assistants de preuve tels que Coq, Isabelle/HOL ou Lean ont ouvert des voies de recherche prometteuses à la frontière de plusieurs disciplines théoriques. Nous proposons de combiner ces paradigmes dans un domaine de recherche en informatique théorique qui s'y prête idéalement : la théorie de la réécriture catégorielle compositionnelle, une généralisation moderne de l'approche algébrique de la réécriture de graphes.

Depuis les travaux pionniers d'Ehrig et al. au début des années 1970, avec comme étape essentielle l'introduction de la théorie des catégories adhésives par Lack et Sobocinski au début des années 2000, l'approche de la réécriture catégorielle permet de traiter une grande variété de systèmes ayant un intérêt pratique et théorique et s'est imposée de facto comme l'approche standard dans le domaine. Une particularité de la réécriture catégorielle concerne la nature des lemmes et des preuves dans ce formalisme, qui utilisent de façon intensive les diagrammes commutatifs et le calcul diagrammatique. Cette particularité incite naturellement à développer une approche appropriée pour exploiter ce raisonnement mathématique fortement modulaire dans le cadre de développements formels dans Coq et explorer la possibilité d'interagir avec Coq sous forme de diagrammes.
L'un des principaux objectifs de ce projet concerne le développement et la gestion d'un système wiki interactif basé sur Coq pour la théorie de la réécriture catégorielle, visant à la fois à certifier et à préserver les connaissances dans ce domaine de recherche dans un format moderne et librement accessible.


Description du projet de doctorat

Le projet a plusieurs objectifs principaux : développer un cadre de « règles de raisonnement diagrammatique » pour les preuves diagrammatiques dans la théorie des catégories, implémenter ce calcul dans l'assistant de preuve Coq, et développer une bibliothèque de preuves diagrammatiques pour la théorie de la réécriture compositionnelle. Le point de départ de cette recherche sera les avancées récentes réalisées par l'équipe CoREACT sur les calculs de croquis conditionnels et généralisés. Les objectifs théoriques du projet de thèse se concentrent sur l'exploration de la méthodologie des « règles de raisonnement diagrammatique » dans le contexte de la théorie des catégories, y compris la théorie des catégories simples, la théorie des catégories doubles, les concepts fibrationnels et, finalement, la théorie de la réécriture catégorielle. Cette exploration permettra d'approfondir la compréhension théorique des preuves diagrammatiques dans ces domaines.

Le deuxième objectif est l'implémentation pratique du calcul des « règles de raisonnement diagrammatique » dans l'assistant de preuve Coq. Cela implique le développement d'une représentation efficace du calcul dans Coq et la création d'une bibliothèque complète de preuves diagrammatiques adaptées à la théorie de la réécriture compositionnelle. L'objectif est de faciliter le raisonnement automatisé et la vérification des preuves, en améliorant l'utilisation des méthodes de preuves diagrammatiques dans les processus de vérification formelle. Le développement s'appuiera sur l'éditeur diagrammatique YADE, qui possède certaines caractéristiques prototypiques de mécanisation de Coq pour la théorie des catégories (cf. https://hal.science/hal-04407118v1).

Globalement, ce projet ambitionne de faire progresser les aspects théoriques et pratiques des calculs de preuves diagrammatiques, en fournissant des outils et des connaissances utiles aux chercheurs et aux praticiens des méthodes formelles et de la théorie des catégories.

Contexte de travail

Le projet ANR CoREACT (2023-2027) est un projet de recherche national entre l'Université Paris Cité (IRIF), l'École Polytechnique (LIX), l'ENS Lyon (LIP), et l'INRIA Sophia-Antipolis (cf. https://coreact.wiki/ pour une liste complète des membres du consortium). Le projet est organisé de manière hautement collaborative, avec des échanges actifs entre toutes les équipes du consortium et des réunions régulières en ligne et en personne. Le poste de doctorant sera co-supervisé par Nicolas Behr (CNRS et Université Paris Cité, IRIF) et Ambroise Lafont (LIX, PARTOUT), l'institution d'accueil principale étant l'IRIF. Le projet bénéficiera d'un financement pour assister à des conférences nationales et internationales, en plus des activités de formation doctorale fournies par l'École Doctorale 386 (Université Paris Cité).

IRIF (PPS) : L'équipe Preuves, Programmes et Systèmes de l'IRIF accueille des chercheurs et des étudiants d'horizons scientifiques variés (en informatique et en mathématiques) sur le thème des fondements et de la pratique des langages de programmation et des systèmes distribués. PPS développe également des méthodes et des outils pour la modélisation des systèmes biologiques et de nouvelles méthodes pour le développement et la maintenance de systèmes dans un cadre de logiciel libre. Enfin, PPS est un acteur majeur dans le domaine des assistants de preuve. PPS dirige également le projet PiCube avec l'INRIA et joue un rôle crucial, en collaboration avec l'INRIA et l'UPMC.

LIX (PARTOUT) : L'équipe PARTOUT explore les formalismes déductifs et computationnels, en se concentrant sur une méta-théorie fiable et vérifiable. L'équipe étudie les propriétés combinatoires et la théorie de la complexité de ces formalismes, ainsi que la nature essentielle de ces formalismes, tels que l'identité de preuve, qui demande quand deux preuves du même théorème sont identiques. Cette question fondamentale reste sans réponse dans la théorie de la preuve. En outre, PARTOUT examine les questions méta-théoriques fondamentales des systèmes logiques et des systèmes de types, y compris l'élimination des coupures, la focalisation, la solidité des types et les théorèmes de normalisation. Cette recherche met l'accent sur les relations entre le calcul et la déduction, au-delà de la correspondance Curry-Howard. En particulier, une méthodologie clé consiste à interpréter le calcul comme une déduction et vice versa, ce qui conduit à des questions de recherche à la fois théoriques et pratiques.