LogoLogo

Spadotti, Régis. Une théorie mécanisée des arbres réguliers en théorie des types dépendants

Spadotti, Régis (2016). Une théorie mécanisée des arbres réguliers en théorie des types dépendants.

[img]
Preview
PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
3651Kb

Résumé en francais

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq.

Sous la direction du :
Directeur de thèse
Bodeveix, Jean-Paul
Filali, Mamoun
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Assistant de preuve - Arbre régulier - Terme cyclique - Co-induction - Transducteur d'arbres
Sujets :Informatique
Déposé le :10 Mar 2017 11:12