Maps: Total and Partial Maps


Perm: Basic Techniques for Permutations and Ordering

Sort: Insertion Sort

Multiset: Insertion Sort With Multisets

Selection: Selection Sort, With Specification and Proof of Correctness

SearchTree: Binary Search Trees

ADT: Abstract Data Types

Extract: Running Coq programs in ML

Redblack: Implementation and Proof of Red-Black Trees

Trie: Number Representations and Efficient Lookup Tables

Priqueue: Priority Queues

Binom: Binomial Queues

Decide: Programming with Decision Procedures

Color: Graph Coloring