Type classes in Coq
Type classes are a very useful mechanism to write programs on abstract structures and support notational abuse by overloading. That's ample good reason to have them in a proof-assistant like Coq. I implemented with Nicolas Oury a port of type classes in Coq [1] and some libraries using the system: a port of the Haskell prelude, a development of category theory and the beginning of order theory. If you would like to take any of these to the next step or have any kind of reaction after seeing them I will gladly answer your mail. I've also given some talks about classes and setoid rewriting [2], [3].
First-Class Type Classes in TPHOLs. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of LNCS. Springer, August 2008, pp.278-293.
First-Class Type Classes, in Coq. Matthieu Sozeau, Talk given at the ProVal workgroup, Orsay, 3rd March 2008.
First-Class Type Classes. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 3rd November 2008.
Valid XHTML 1.1! Valid CSS!