# 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, coq)
nwtb invariant for DFS in undirected graph (proof)
Random search walk (proof1, proof2)
Abstract depth first search (proof1, proof2, proof1b, proof2b,
coq)
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