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. +
+
+ 
+