| layout | title |
|---|---|
default |
About |
Math-Classes is a library of abstract interfaces for mathematical structures, such as
- Algebraic hierarchy (groups, rings, fields, ...)
- Relations, orders, ...
- Categories, functors, universal algebra, ...
- Numbers: ℕ, ℤ, ℚ, ...
- Operations, ...
It's heavily based on Coq's new TypeClasses.
in order to archieve:
- elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory);
- a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheritance, all trivial;
- clean expression terms that neither refer to proofs nor require deeply nested record projections;
- fluent rewriting;
- easy and flexible replacement and specialization of data representations and operations with more efficient versions;
- ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.
More information can be found here:
- Presentation
- Paper
You can find the latest code on github