- Notifications
You must be signed in to change notification settings - Fork7
Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
License
NotificationsYou must be signed in to change notification settings
coq-community/fav-ssr
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
A port of the bookhttps://functional-algorithms-verified.org/ to Coq/SSReflect.
The book was previously called "Functional Algorithms Verified", hence the FAV acronym.
- 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
To build manually, do:
make# or make -j <number-of-cores-on-your-machine>- Binary Trees
- Binary Search Trees
- Abstract Data Types
- 2-3 Trees
- Red-Black Trees
- AVL Trees
- Beyond Insert and Delete: \cup, \cap and -
- Arrays via Braun Trees
- Tries
- Region Quadtrees
- Dynamic Programming
- Amortized Analysis
- Queues
- Splay Trees
- Skew Heaps
- Pairing Heaps
- Knuth–Morris–Pratt String Search
- Huffman’s Algorithm
- Alpha-Beta Pruning