Sorting algorithms
Selection sort (proof1, proof2)
Bubble sort (proof1, proof2)
Insertion sort (proof1,
proof2; proof3). Stability (proof4)
Insertion sort in lists (proof1, proof2)
Insertion in sorted trees (proof1, proof2).
Quicksort (proof,
coq1,
coq2)
Mergesort on lists (proof1,
proof2)
Mergesort (proof1, proof2;
coq1,
coq2
)
Jean-Jacques Lévy
Chen Ran