Functional Data Structures and Algorithms in SSReflect

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

The book was previously called "Functional Algorithms Verified", hence the FAV acronym.

Meta

• Author(s):
  • Alex Gryzlov (initial)
• Coq-community maintainer(s):
  • Alex Gryzlov (@clayrat)
• License: MIT license
• Compatible Coq versions: 8.15 to 8.19
• Additional dependencies:
  • MathComp ssreflect 1.17.0 to 1.19.0
  • MathComp algebra
  • Equations 1.3 or later
• Coq namespace: favssr
• Related publication(s): none

Building instructions

To build manually, do:

make   # or make -j <number-of-cores-on-your-machine>

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. Region Quadtrees

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

Part V: Selected Topics

24. Knuth–Morris–Pratt String Search
25. Huffman’s Algorithm
26. Alpha-Beta Pruning