LogoLogo

Picard, Célia. Représentation coinductive des graphes

Picard, Célia (2012) Représentation coinductive des graphes.

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

Résumé en francais

Nous nous intéressons à la représentation de graphes dans le prouveur Coq. Nous avons choisi de les représenter par des types coinductifs dont nous voulions explorer l'utilisation. Ceux-ci permettent de rendre succincte et élégante la représentation et d'obtenir la navigabilité par construction. Nous avons dû contourner la condition de garde dont le but est d'assurer la validité des opérations effectuées sur les objets coinductifs. Son implantation dans Coq est restrictive et interdit parfois des définitions sémantiquement correctes. Une formalisation canonique des graphes dépasse ainsi l'expressivité directe de Coq. Nous avons donc proposé une solution respectant ces limitations, puis nous avons défini une relation sur les graphes nous permettant d'obtenir la même notion d'équivalence qu'avec une représentation classique tout en gardant les avantages de la coinduction. Nous montrons qu'elle est équivalente à une relation basée sur des observations finies.

Sous la direction du :
Directeur de thèse
Matthes, Ralph
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 :Coinduction - Prouveur de théorèmes - Graphes - Listes - Mélange induction et coinduction
Sujets :Informatique
Déposé le :16 Oct 2012 11:28