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.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Bas Spitters, Eelis van der Weegen
• Keywords: Formalization Includes Portions, ITP 2010, Mathematics, Sound Abstract Interfaces, Type Class Mechanism