Type classes for mathematics in type theory
Weegen, E.E. van der
- Publisher: CAMBRIDGE UNIV PRESS
Mathematical Structures in Computer Science
(issn: 0960-1295, eissn: 1469-8072)
Computer Science - Logic in Computer Science
The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to m...