Research
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.