Preface

Basic Techniques for Comparisons and Permutations    (Perm)

Insertion Sort    (Sort)

Insertion Sort Verified With Multisets    (Multiset)

Insertion Sort With Bags    (BagPerm)

Selection Sort    (Selection)

Merge Sort, With Specification and Proof of Correctness    (Merge)

Binary Search Trees    (SearchTree)

Abstract Data Types    (ADT)

Running Coq Programs in OCaml    (Extract)

Red-Black Trees    (Redblack)

Number Representations and Efficient Lookup Tables    (Trie)

Priority Queues    (Priqueue)

Binomial Queues    (Binom)

Programming with Decision Procedures    (Decide)

Graph Coloring    (Color)