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 équatione...
| Main Author: | |
|---|---|
| Language: | fra |
| Published: |
Université de Grenoble
2012
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00683661 http://tel.archives-ouvertes.fr/docs/00/68/36/61/PDF/these-braibant_archivage_2012.pdf |