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)
- Total and Partial Maps
- Sections
- Program for Binary Search Trees
- Search Tree Examples
- What Should We Prove About Search trees?
- Efficiency of Search Trees
- Proof of Correctness
- Correctness Proof of the elements Function
- Representation Invariants
- Preservation of Representation Invariant
- We Got Lucky
- Every Well-Formed Tree Does Actually Relate to an Abstraction
- It Wasn't Really Luck, Actually
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)
This page has been generated by coqdoc