# 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

GraphSet module (proof)
Abstract depth first search (white initial color) (proof1,
proof2; proof3, proof4)
The white-path theorem for depth first search (proof == sound + complete)
The white-path theorem for depth first search [with black and gray sets] (proof == sound + complete)
Abstract DFS: no white to black edge for undirected graph (proof)

Random search walk (sound +
complete;
sound2)
Breadth first search (sound,
complete)
Iterative depth first search with a stack (sound,
complete)

Depth first search (mutable visited set) (sound,
complete)
Depth first search (list of vertices + mutable visited set) (sound,
complete)
Depth first search (list of vertices + mutable visited set + color) (sound,
complete)
Depth first search as in Sedgewick (sound,
complete;
with graph array sound;
complete)

Strongly connected components - Tarjan 1972 (with ranks and
explicit grays) (proof1)
SCC - Tarjan 1972 (with just ranks) (weak, strong)
SCC - Tarjan 1972 (with precedes) (weak, strong) [ a ]
Strongly connected components - Tarjan 1972 (quasi imperative)
(proof)
Strongly connected components - Kosaraju 1978 (abs) (proof)

Articulation points (weak,
strong)
Biconnected components (weak,
strong)
Acyclicity test (functional,
imperative)

Jean-Jacques Lévy

Chen Ran