Pierre Letouzey edited this page Oct 18, 2017 · 20 revisions
Clone this wiki locally

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.

Software Verified in 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

Other Algorithms