Computer Science – Logic in Computer Science
Scientific paper
2011-02-07
Computer Science
Logic in Computer Science
Scientific paper
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 make practical a particularly flexible approach formerly thought infeasible. Thus, we address both traditional proof engineering 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 minimum. The base of our development consists of type classes representing a standard algebraic hierarchy, as well as portions of category theory and universal algebra. On this foundation we build a set of mathematically sound abstract interfaces for different kinds of numbers, succinctly expressed using categorical language and universal algebra constructions. Strategic use of type classes lets us support these high-level theory-friendly definitions while still enabling efficient implementations unhindered by gratuitous indirection, conversion or projection. Algebra thrives on the interplay between syntax and semantics. The Prolog-like abilities of type class instance resolution allow us to conveniently define a quote function, thus facilitating the use of reflective techniques.
der Weegen Eelis van
Spitters Bas
No associations
LandOfFree
Type Classes for Mathematics in Type Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Type Classes for Mathematics in Type Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Type Classes for Mathematics in Type Theory will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-681397