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.
