In September 2012, I started a post-doc in the Gallium team, at Inria Rocquencourt.
During my PhD, we released a reflexive tactic for deciding Kleene algebras; the current state of the corresponding library (ATBR) can be found here. We also implemented tools for rewriting modulo AC in Coq; the current state of the corresponding library can be found here.
Toward the end of my PhD, I implemented a Coq library for verifying hardware; the (outdated) state of the corresponding library can be found here.
My current research interests involve the use of the Coq proof assistant to verify hardware components.