Preface

Basic Techniques for Permutations and Ordering    (Perm)

Insertion Sort    (Sort)

Insertion Sort With Multisets    (Multiset)

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

Binary Search Trees    (SearchTree)

Abstract Data Types    (ADT)

Running Coq Programs in OCaml    (Extract)

Implementation and Proof of 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)