# 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
)
# Graph algorithms

Abstract depth first search (white initial color) (proof1,
proof2; proof3, proof4)
Abstract depth first search (proof, sound, complete)
Abstract depth first search [with black and gray sets] (proof, sound, complete)
No white to black edge in DFS for undirected graph (proof)
Random search walk (sound,
complete,
sound2)
Breadth first search (proof)
Iterative depth first search with stack (proof)
GraphSet module (proof)
Depth first search (array + list) (proof)
Depth first search as in Sedgewick (proof)
Strongly connected components - Tarjan 1972 (abs) (proof1, proof2, proof3)
Strongly connected components - Tarjan 1972 (quasi imperative)
(proof)
Strongly connected components - Kosaraju 1978 (abs) (proof)
Acyclicity test (abs) (proof)

Jean-Jacques Lévy

Chen Ran