Situation

I defended my PhD on the the 17th of February 2012. This PhD was supervised by Damien Pous and Jean-Bernard Stefani in the team Sardes of Inria Grenoble - Rhône-Alpes.

Starting in April, I shall make a visit at CSAIL, in Adam Chlipala's group.

PhD

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.

Research

My current research interests involve the use of the Coq proof assistant to verify hardware components.

Tools

I am a happy user of the Coq proof assistant, and do most of my software developments in OCaml.