By Eelis van der Weegen and Bas Spitters.
We have been working on a new set of foundational interfaces for formalized constructive mathematics in Coq, heavily based on Coq's new type classes, used in a systematic way in order to achieve:
We have submitted a paper (PDF) presenting our development for the MSCS Special Issue on Advances and Perspectives in the Mechanization of Mathematics.
We have submitted a "rough diamond" extended abstract (PDF) presenting our development for ITP-10.
The development can be browsed and downloaded at the GitHub repository at
http://github.com/Eelis/math-classes/
(Click the "Download Source" button for a tarball containing all the source code.)
Alternatively, you can browse the coqdoc-generated documentation.