Return to search

Algèbres de Kleene, réécriture modulo AC et circuits en coq

Cette thèse décrit trois travaux de formalisation en Coq. Le premier chapitre s'intéresse à l'implémentation d'une procédure de décision efficace pour les algèbres de Kleene, pour lesquelles le modèle des langages réguliers est initial : il est possible de décider la théorie équationelle des algèbres de Kleene via la construction et la comparaison d'automates finis. Le second chapitre est consacré à la définition de tactiques pour la réécriture modulo associativité et commutativité en utilisant deux composants : une procédure de décision réflexive pour l'égalité modulo AC, ainsi qu'un greffon OCaml implémentant le filtrage modulo AC. Le dernier chapitre esquisse une formalisation des circuits digitaux via un plongement profond utilisant les types dépendants de Coq ; on s'intéresse ensuite à prouver la correction totale de circuits paramétriques.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00683661
Date17 February 2012
CreatorsBraibant, Thomas
PublisherUniversité de Grenoble
Source SetsCCSD theses-EN-ligne, France
Languagefra
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds