Publications - Math Classes

Papers

First-class type classes, Matthieu Sozeau and Nicolas Oury. In TPHOLs 2008, volume 5170 of LNCS, pages 278–293, 2008. [pdf]
Type classes for mathematics in type theory, Bas Spitters and Eelis van der Weegen. In MSCS, special issue on “Interactive theorem proving and the formalization of mathematics”, 2011. (A shorter version “Developing the algebraic hierarchy with type classes in Coq” appeared as a Rough Diamond at ITP-10) [arXiv]
Type classes for efficient exact real arithmetic in Coq, Robbert Krebbers and Bas Spitters. Submitted, 2011. [arXiv]
Computer certified efficient exact reals in Coq, Robbert Krebbers and Bas Spitters. In Proceedings of Calculemus/MKM 2011, volume 6824 of LNAI, pages 90–106, 2011. [arXiv]

Type Classes for Mathematics, Robbert Krebbers (with Bas Spitters and Eelis van der Weegen). At Workshop on reification and generic tactics, March 31, 2011, INRIA Paris. [pdf]
Developing the algebraic hierarchy with type classes in Coq, Eelis van der Weegen (with Bas Spitters). At the Coq workshop, 9 July, 2010, FLOC 2010, Edinburgh. [pdf]