The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

There is UniMath https://github.com/UniMath/UniMath in particular algebra1a,b,c,d in https://github.com/UniMath/UniMath/tree/master/UniMath/Foundations/hlevel2 .

There is a partial description of the Foundations part of the UniMath here http://arxiv.org/abs/1401.0053 .

Vladimir.

On Nov 9, 2014, at 1:21 AM, 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