Sciweavers

Share
ITP
2010

Developing the Algebraic Hierarchy with Type Classes in Coq

8 years 7 months ago
Developing the Algebraic Hierarchy with Type Classes in Coq
We present a new formalization of the algebraic hierarchy in Coq, exploiting its new type class mechanism to make practical a solution formerly thought infeasible. Our approach addresses both traditional challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which ion penalties inhibiting efficient computation are reduced to a imum. To support mathematically sound abstract interfaces for N, Z, and Q, our formalization includes portions of category theory and multisorted universal algebra.
Bas Spitters, Eelis van der Weegen
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2010
Where ITP
Authors Bas Spitters, Eelis van der Weegen
Comments (0)
books