I have finished my Ph.D.. 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.