The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I am looking for a framework which allows me to reason about basic algebraic 
structures, in particular semirings, rings, ordered rings, etc. in Coq. Type 
hierarchy, basic Properties, etc. I could not find anything readily available 
for Coq, except this paper:

[1] H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, “A Constructive 
Algebraic Hierarchy in Coq,” J. Symb. Comput., vol. 34, no. 4, pp. 271–286, 
Oct. 2002.

If there are any other libraries I should look at, or should I try to extract 
required structures from FTA project?
I started putting together simple placeholder of my own, but I quickly 
realized that this is too much work and beyond the scope of my project and I 
would rather re-use something already available. 

Sincerely,
Vadim