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

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

Other Algorithms

FormalizedAndVerified (last edited 06-04-2010 10:53:36 by oumix)

Cocorico!WikiLicense