FormalizedAndVerified - rocq-prover/rocq GitHub Wiki
Mathematics Formalized in Coq
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
Software Verified in Coq
Sorting
| Algorithm | Formalisation available from |
|---|---|
| Quicksort | Why |
| Treesort | StandardLibrary |
| Insertion sort | CoqArt chapter 1 |
| Selection sort | Why |
| Maximum sort | Why |
| Heapsort | Why |
| Mergesort | Xavier Leroy |