Réécriture basée sur Coq : vers une théorie des catégories appliquée exécutable – CoREACT

L'émergence récente de la théorie appliquée des catégories (ACT), ainsi que les projets à grande échelle de formalisation des mathématiques à l'aide d'assistants de preuve tels que Coq, Isabelle/HOL ou Lean, ont ouvert des voies de recherche prometteuses, à la croisée 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égorique compositionnelle, généralisation moderne de l'approche algébrique de la réécriture de graphes. Partant des travaux pionniers d'Ehrig et al. au début des années 1970, avec comme jalon clé l'introduction de la théorie des catégories adhésives introduite par Lack et Sobocinski au début des années 2000, l'approche catégorique de la réécriture permet de traiter une grande variété de systèmes d'intérêt pratique et théorique, et s'est de facto imposée comme l'approche standard dans le domaine. Une particularité de la réécriture catégorique réside dans la nature des lemmes et des preuves dans ce formalisme, qui font intensivement usage de diagrammes commutatifs et d'un calcul diagrammatique sur ces derniers. Cela incite naturellement à développer approche appropriée qui permettrait d'exploiter ce type de raisonnement mathématique hautement modularisé au sein de développements formels en Coq, ainsi qu'à explorer la possibilité d'interagir avec Coq sous forme diagrammatique. L'un des objectifs principaux de ce projet est de réunir une équipe d'experts du domaine ainsi qu'un groupe d'intérêt international en ligne visant à développer et à maintenir un système Wiki interactif, basé sur Coq, pour la théorie de la réécriture catégorique, visant à la fois à certifier et à conserver les connaissances dans ce domaine de recherche dans un format moderne et librement accessible.