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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00683661 |
| Date | 17 February 2012 |
| Creators | Braibant, Thomas |
| Publisher | Université de Grenoble |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | fra |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0021 seconds