Developing the algebraic hierarchy with type classes in Coq

Abstract

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 abstraction penalties inhibiting efficient computation are reduced to a bare minimum. To support mathematically sound abstract interfaces for ℕ, ℤ and ℚ, our formalization includes portions of category theory and multisorted universal algebra. © 2010 Springer-Verlag.