-
Notifications
You must be signed in to change notification settings - Fork 7
/
meta.yml
116 lines (98 loc) · 2.87 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
---
fullname: Functional Data Structures and Algorithms in SSReflect
shortname: fav-ssr
opam_name: coq-fav-ssr
organization: coq-community
community: true
action: true
branch: trunk
dune: false
synopsis: A port of the Functional Data Structures and Algorithms book to Coq/SSReflect
description: |-
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.
authors:
- name: Alex Gryzlov
initial: true
maintainers:
- name: Alex Gryzlov
nickname: clayrat
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: MIT license
identifier: MIT
supported_coq_versions:
text: 8.15 to 8.19
opam: '{>= "8.15" & < "8.20"}'
tested_coq_opam_versions:
- version: '1.19.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '1.18.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.15'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "1.17" & < "2.0"}'
description: |-
[MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-equations
version: '{>= "1.3"}'
description: |-
[Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
namespace: favssr
keywords:
- name: program verification
categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
build: |-
## Building instructions
To build manually, do:
```shell
make # or make -j <number-of-cores-on-your-machine>
```
documentation: |-
## Contents
1. [Basics](src/basics.v)
### Part I: Sorting and Selection
2. [Sorting](src/sorting.v)
3. [Selection](src/selection.v)
### Part II: Search Trees
4. [Binary Trees](src/bintree.v)
5. [Binary Search Trees](src/bst.v)
6. [Abstract Data Types](src/adt.v)
7. [2-3 Trees](src/twothree.v)
8. [Red-Black Trees](src/redblack.v)
9. [AVL Trees](src/avl.v)
10. [Beyond Insert and Delete: \cup, \cap and -](src/beyond.v)
11. [Arrays via Braun Trees](src/braun.v)
12. [Tries](src/trie.v)
13. [Region Quadtrees](src/quadtree.v)
### Part III: Priority Queues
14. [Priority Queues](src/priority.v)
15. [Leftist Heaps](src/leftist.v)
16. [Priority Queues via Braun Trees](src/braun_queue.v)
17. [Binomial Heaps](src/binom_heap.v)
### 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](src/huffman.v)
26. Alpha-Beta Pruning
---