FormalizedAndVerified
There is a great deal of mathematics already formalized in Coq. Some of the material is available in the StandardLibrary or in the Coq's repository of user contributions.
- Top100MathematicalTheoremsInCoq: a list of theorems among the Top 100 Mathematical Theorems that are formalised in Coq (see also http://www.cs.ru.nl/~freek/100/).
- CoRN : a large library of formalised mathematics built on top of Coq
| Algorithm | Formalisation available from |
|---|---|
| Quicksort | Why |
| Treesort | StandardLibrary |
| Insertion sort | CoqArt chapter 1 |
| Selection sort | Why |
| Maximum sort | Why |
| Heapsort | Why |
| Mergesort | Xavier Leroy |
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.