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 ML    (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)