Functional Algorithms Verified in SSReflect

A port of https://functional-algorithms-verified.org/ to Coq/SSReflect.

Besides Mathcomp, this also requires the Equations plugin.

Contents

1. Basics

Part I: Sorting and Selection

2. Sorting
3. Selection

Part II: Search Trees

4. Binary Trees
5. Binary Search Trees
6. Abstract Data Types
7. 2-3 Trees
8. Red-Black Trees
9. AVL Trees
10. Beyond Insert and Delete: \cup, \cap and -
11. Arrays via Braun Trees
12. Tries
13. Huffman’s Algorithm

Part III: Priority Queues

14. Priority Queues
15. Leftist Heaps
16. Priority Queues via Braun Trees
17. Binomial Heaps

Part IV: Advanced Design and Analysis Techniques

18. Dynamic Programming
19. Amortized Analysis
20. Queues
21. Splay Trees
22. Skew Heaps
23. Pairing Heaps