IRIT - UMR 5505

Avec une expérience de co-développement de théories et de leurs formalisations en Coq qui sont publiables et partiellement publiées, on veut commencer à outiller des théories en Coq qui n'ont pas été conçues sous l'angle de leur formalisabisation. Il n'existe pas encore une implantation généralement acceptée de la théorie des catégories (en Coq, il y en a deux très complémentaires), et on vise des formalisations adaptées à nos domaines d'application. Un projet ANR en collaboration avec l'Onera a été soumis sur la modélisation catégorielle de systèmes de systèmes. On veut simultanément implanter et certifier les résultats théoriques sur la réécriture de graphes attribués de la thèse de Rebout 05-08. Techniquement, on veut bénéficier du polymorphisme dans la modélisation (qui n'existe en Java que depuis la version 5, mais qui est la clé à la modélisation par Coq). Quand on passe des arbres vers des graphes, des structures coinductives sont proposées par Coq. Cependant, il faut dépasser ou contourner les limites actuelles de Coq en ce qui concerne les définitions corecursives acceptées (thèse Picard 08-). L'approche propre à la théorie des catégories de structurer le raisonnement sur les obligations équationnelles de preuve est la commutativité de diagrammes qu'il faut outiller dans le respect du savoir-faire des théoriciens. On veut également s'approprier des technologies nouvelles de représentation de variables liées (parmi eux l'approche par types de données imbriqués), en implantant nos propres résultats théoriques (par exemple des traductions CPS). Évidemment, toutes les retombées théoriques de nos travaux d'outillage et d'implantation seront à identifier, isoler et valoriser.