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)