Nos partenaires

CNRS

Rechercher





Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe ACADIE > Recherches

Type Theory and Category Theory

The principal goal of our work based on concepts of Type Theory and Category Theory is the improvement and development of methods of program verification and certification. Our research in this domain started in 1998 and was extended thanks to the arrival of new members and several PhD students. The relation between theory and applied methods always has always been bi-directional, theoretical concepts helped to develop or improve the applications and the study of well-chosen concrete questions has enriched the theory.

In the period 2009-2014 there was a continuation and completion of research started earlier and exploration/solution of new problems. We worked on the problem of termination of recursive programs via typability with the aim of extending the domain of applicability of certified recursion schemes ; coinduction, including representation of graphs and graph transformations in type theories ; formalization and verification in proof assistants.

The main applications of this theoretical work are the formalization and techniques for interactive verification of pointer-manipulating code and logical methods for proving graph transformations.

Since 2012, to an important extent, our research in this axis has been structured by the ANR project "Categorical and Logical Methods in Model Transformation" (CLIMT). In our work on a category- and type-theory based approach to attributed graph transformation, the main novelty is that type theory is used in the representation of attributes and attribute computations. Within the project, we also studied a coinductive representation of graphs, where we solved the problem of embedded lists in a coinductive data type. In collaboration with the other project partner, we have started identifying decidable assertion logics for graph transformation programs.

A line of research (started earlier) on coercive subtyping (involving categorical coherence and conservativity in type theory) was essentially completed in 2013. We continued the work on verification of commutativity of categorical diagrams using proof-theoretical methods, notably, in case of non-free categories. On the side of the connection of logic and computation, we worked on monadic and continuation-passing style transformations and a coinductive analysis of proof search in propositional logic. Concerning ongoing work, we have established contacts with researchers working on Homotopy Type Theory and Univalent Foundations (Princeton), with the view that new foundations may be useful for the development of more efficient proof assistants. We have also started to explore the notion of conditional invertibility (with links to practically important reversible computation research), with category-theoretical conditions.