The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I use the MathClasses library (via the corn project).

https://coq.inria.fr/cocorico/MathClasses

http://corn.cs.ru.nl/

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, Nov 8, 2014 at 8:21 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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