Bibtex de la publication

@PhDThesis{ Sp2016.1,
author = {Spadotti, Régis},
title = "{Une théorie mécanisée des arbres réguliers en théorie des types dépendants}",
year = {2016},
month = {mai},
type = {Thèse de doctorat},
school = {Université Paul Sabatier},
address = {Toulouse, France},
language = {francais},
note = {(Soutenance le 19/05/2016)},
abstract = {Les assistants de preuve sont des outils développés dans le but d'aider les informaticiens à raisonner formellement. En effet, ces outils fournissent un cadre permettant l'expression d'énoncés et de propriétés dans un langage formel. Ensuite, en utilisant les règles de preuve de la logique sous-jacente, des théorèmes sont prouvés puis vérifiés mécaniquement par la machine. La théorie des types dépendants est un formalisme qui peut servir comme alternative à la théorie des ensembles comme fondation pour exprimer les mathématiques. Principalement, cela signifie que le même langage est utilisé pour définir des programmes, énoncer leurs spécifications et prouver leurs corrections. Entre autres choses, la théorie des types offre de puissants principes de raisonnement comme l'induction pour les objets finis et la coinduction pour les objets potentiellement infinis. Les graphes sont des structures de données très répandues en informatique. Ils sont utilisés pour donner des sémantiques à diverses logiques, pour modéliser des opérations ou exprimer des relations entre des objets. En particulier, les graphes offrent un formalisme pour exprimer des structures acycliques ainsi que des structures cycliques. Raisonner sur les graphes en théorie des types est une tâche complexe. La principale raison est due au fait que les graphes sont, en général, des structures qui ne sont pas définies inductivement. En tant que tels, ils ne peuvent pas être encodés directement par des types inductifs. Cependant, les types coinductifs — qui offrent un cadre permettant le traitement des objets infinis en théorie des types — peuvent être utilisés comme une représentation possible de graphes. Nous nous intéressons au problème consistant à mécaniser une théorie des arbres réguliers en théorie des types dépendants. Informellement, les arbres réguliers sont caractérisés comme le sous-ensemble des arbres infinis tels que l'ensemble de leurs sous-arbres distincts est fini. Ainsi, les arbres réguliers peuvent être vus comme des structures cycliques finies. Dans le cadre de cette thèse, nous proposons deux formalisations des arbres réguliers. La première, basée sur la coinduction, définit les arbres réguliers comme la restriction d'un type coinductif. La seconde formalisation suit une approche syntaxique, dans le sens où les arbres réguliers sont caractérisés par des termes cycliques définis inductivement, c'est-à-dire par des termes intégrant des pointeurs de retour. Nous prouvons que ces deux représentations sont isomorphes. Dans un second temps, nous étudions le problème consistant à définir des transformations d'arbres qui préservent la propriété de régularité. Dans ce but, nous exploitons le formalisme des transducteurs d'arbres comme un outil visant à obtenir une caractérisation syntaxique d'un sous-ensemble de fonctions corécursives. Les transducteurs d'arbres sont ensuite interprétés comme des morphismes d'arbres préservant la régularité. Enfin, nous étudions plusieurs résultats de décidabilité via une mécanisation du ¿-calcul propositionnel interprété sur les arbres réguliers. En particulier, nous prouvons la décidabilité de la relation de bissimilarité entre les arbres réguliers au travers d'une réduction vers un problème de model-checking.}
}