GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

No menu could be recovered. Follow the blue links in the page.

This view

  • Original page
  • New address

GeezerVison is showing math-classes.github.io — About - Math Classes

Math Classes
  • About
  • Motivation
  • Publications
  • People
  • Coqdoc
  • Github
  • Wiki
    •

    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, (shift, power, abs, …)

    It is heavily based on Coq’s new type classes in order to provide: structure inference, multiple inheritance/sharing, convenient algebraic manipulation (e.g. rewriting) and idiomatic use of notations.

    Here is a SVG diagram showing all files and their dependencies with links to the coqdoc dependencies.

    Here are two diagrams showing the main components of the algebraic hierarchy and the various orders in math classes.

    Algebraic Hierarchy Order Hierarchy

    Math classes is used in C-CoRN to implement high performance exact real number arithmetic.

    You are visitor 01402503 — GeezerVison does not store the pages you look up.
    Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.