Confluences cubiques et formalisation des catégories cubiques

Cette thèse s'inscrit dans un programme de recherche sur la formalisation de la réécriture. Nous étudions la propriété de confluence, qui garantit que deux réécritures sur une même expression peuvent être prolongées par d'autres chemins de réécriture conduisant à une expression commune. Cette propriété fondamentale de la réécriture a été exprimée dans différents langages: diagrammes, inclusions de relations, algèbres de Kleene, catégories globulaires et cubiques. Cette thèse étudie la formalisation de cette propriété d'un point de vue cubique. Les schémas de confluence de branchements de deux réécritures sont par définition carrés et ceux de k-branchements forment des k-cubes. Cela suggère une formulation naturelle des preuves de confluence dans le langage des catégories et polygraphes cubiques. Dans cette thèse, nous introduisons un cadre permettant d'étudier les preuves de confluence comme des constructions cubiques et d'en déduire des formalisations cubiques à un seul ensemble. Nous explicitons la notion de contraction cubique permettant de démontrer l'acyclicité des (ω,0)-catégories cubiques. Nous montrons comment construire des contractions cubiques à partir de systèmes de réécriture abstraits confluents et terminants. Nous donnons ainsi une construction explicite de résolution polygraphique cubique constituée en toute dimension par les formes cubiques des confluences des multiples branchements. Nous formulons les schémas de preuves de confluence à la Newman et Church-Rosser dans ce langage polygraphique. Nous introduisons les catégories cubiques à un seul ensemble, dites single-set, qui axiomatisent les catégories cubiques en définissant la dimension des cellules par des équations de point fixe. L'axiomatisation à un seul ensemble est bien adaptée à une formalisation dans l'assistant de preuve Isabelle/HOL. Nous formalisons les ω-catégories cubiques à un seul ensemble dans Isabelle/HOL. Enfin, nous formalisons le concept de système de réécriture dans les ω-catégories globulaires polygraphiables à un seul ensemble, qui correspondent aux ω-catégories globulaires librement engendrées par des ω-polygraphes. Nous les caractérisons comme les objets cofibrants de la structure de modèle folk transférée et nous les formalisons dans Isabelle/HOL.