Kleene algebra, Rewriting modulo AC and Circuits in Coq.
Algèbres de Kleene, réécriture modulo AC et circuits en coq
Résumé
This thesis describe three formalisations in Coq. The first chapter is devoted to the implementation of an efficient decision procedure for Kleene algebras : as regular languages form the initial model of Kleene algebras, we can resort to finite automata algorithms to solve equations in an arbitrary Kleene algebra. The second chapter present a set of tools for rewriting modulo associativity and commutativity built using two components: a reflexive decision procedure for equality modulo AC and an OCaml plug-in for pattern matching modulo AC. The third chapter defines a deep-embedding of hardware circuits using dependent types that is used to model and prove the functional correctness of parametrised circuits.
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.
Origine : Version validée par le jury (STAR)