MathClasses

Pierre Letouzey edited this page Oct 12, 2017 · 6 revisions
Clone this wiki locally

Math Classes

math-classes is a library of abstract interfaces for mathematical structures.

  • Algebraic hierarchy (groups, rings, fields, ...)
  • Relations, orders, ...
  • Categories, functors, universal algebra, ...
  • Numbers: NN, ZZ, QQ, ...
  • 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