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 |
|
Treesort |
|
Insertion sort |
|
Selection sort |
|
Maximum sort |
|
Heapsort |
|
Mergesort |