Mathematical Components
-Libraries of formalized mathematics
- - - - - - - - - --About
- -The Mathematical Components library for - Coq has its origins in -the formal proof of the Four Colour Theorem. Since then it has grown -to cover many areas of mathematics and has been used for -large scale projects like the formal proof of the Odd Order Theorem. -
-The library is written using the Ssreflect proof language that is an integral -part of the distribution. -
- --Getting the library
- - The current stable release of the
-Mathematical Components library can be
-downloaded from github.
-
-Older versions of the library are available
-in the historic archive.
-
-Documentation
- --Each source files features a documentation header which -describes the concepts and notations introduced in that file. -The coqdoc presentation of the source files can be browsed online. -
--The library graph can be browsed interactively. -
--The Ssreflect language comes with a dedicated -reference manual. -
-We also wrote a book introducing the techniques for writing -algorithms and proofs and describing the design ideas of the library. -
--Contact
- --Interested? -Subscribe to the ssreflect mailing list -and let us know what you are using our libraries for, ask questions, etc. -You can also browse the archives of the list or consult the -general information page. -
--Authors and Contributors
- -The Mathematical Components library and the Ssreflect proof language -are developed by the -Mathematical Components team, at the -Inria -- Microsoft Research Joint Centre. -
-
- 
-