I'm finishing up my thesis right now and the latest revision of my manuscript can be found here (in french). My thesis is centered around the Russell language which provides facilities for writing dependently-typed programs in Coq. To further improve the usability of the system I also designed a typeclass system for Coq with Nicolas Oury and developed a new setoid rewriting tactic based on it. I also have a page recapitulting all the Coq stuff I did for my thesis or out of curiosity.