文件名称：coq-algs：Coq中经过正式验证的算法和数据结构：概念和技术
文件大小：629KB
文件格式：ZIP
更新时间：2024-02-29 05:42:41
algorithms thesis functional-programming coq data-structures
辅酶 您好。 该存储库包含一些随机的Coq代码，其中大多数与纯功能算法和数据结构有关。 它还包含我的硕士论文，也与算法有关。 开发的结构如下： RCCBase.v包含一些基本策略和辅助材料。 ADT /包含抽象数据类型的接口，例如队列，优先级队列，集合，有限映射等。 Data /包含基本归纳数据类型的实现，其中大多数是树。 这些基本树然后用于实现数据结构。 DS /包含数据结构，例如BST，堆，序列等。 记忆/是记忆功能的la脚尝试。 没什么值得一看的。 反射/在反射证明上有一些代码，也很la脚。 Sorting /包含各种排序算法的实现。 结构/具有排序和反射所需的代数和阶理论结构的实现。 垃圾/是垃圾。 甚至都不要看。 已完成 Structures /包含LinDec （可确定的线性顺序的实现），可用于大多数排序算法，以及一些词条和功能强大的自动化策略dec（称为d
【文件预览】：
coq-algs-master
----RCCBase.v(4KB)
----Structures()
--------UCRing.v(4KB)
--------CMon.v(1KB)
--------Ord.v(16KB)
----Trash()
--------BinomialTreeTrash.v(6KB)
--------Prod.v(471B)
--------LList.v(4KB)
--------LazyList.v(648B)
--------Enumerable.v(2KB)
--------Positional.v(3KB)
--------LazyEvalTest.v(3KB)
--------LList2.v(5KB)
--------DFA.v(2KB)
----ADT()
--------Sequence.v(2KB)
--------Queue.v(6KB)
--------FinSet.v(1KB)
--------Sortable.v(7KB)
--------FinSet2.v(874B)
--------Queue()
--------Deque.v(3KB)
--------PriorityQueue.v(6KB)
--------Stack.v(2KB)
--------PartialFinMap.v(1KB)
----TODO(741B)
----DS()
--------BST2.v(8KB)
--------EasyFingerTree.v(8KB)
--------Heap.v(3KB)
--------Heap()
--------BST.v(29KB)
--------FingerTree.v(2KB)
--------Okasaki_Ch10.v(17KB)
--------BHeap.v(11KB)
--------Deque.v(20KB)
--------BST()
----Sorting()
--------MsQsUnited.v(1KB)
--------Perm.v(11KB)
--------RedblackSort.v(4KB)
--------SplaySort.v(4KB)
--------GeneralizedSelectionSort.v(2KB)
--------MergeSortSpec.v(1KB)
--------Sort.v(6KB)
--------QuickSort.v(6KB)
--------MergeSort.v(8KB)
--------TreeSort.v(3KB)
--------BraunMergeSort.v(3KB)
--------SortSpec.v(2KB)
--------Mergesort2.v(2KB)
--------Test.v(4KB)
--------SelectionSort.v(10KB)
--------QuicksortSpec.v(4KB)
--------PairingSort.v(3KB)
--------InsertionSort.v(3KB)
--------GeneralizedInsertionSort.v(1KB)
----Reflection()
--------Reflection_a_la_carte.v(8KB)
--------CMonRefl.v(20KB)
--------Test()
--------UCRingRefl.v(20KB)
--------ReflectionClass.v(2KB)
--------Formula2.v(6KB)
--------CMonRefl2.v(6KB)
--------ReflectionLtac.v(2KB)
--------Formula.v(6KB)
--------MonRefl_NBE.v(1KB)
----Thesis()
--------Thesis.tex(160KB)
--------Trash()
--------Thesis.pdf(428KB)
--------Snippets()
--------minted.sty(46KB)
--------buildthesis.sh(106B)
--------iithesis.cls(10KB)
----.gitignore(175B)
----Memoization()
--------Memoize2.v(2KB)
--------Memoize.v(8KB)
----README.md(4KB)
----build.sh(242B)
----Data()
--------Tree.v(8KB)
--------BTree.v(33KB)
--------ListLemmas.v(8KB)
--------EBTree.v(7KB)
--------NonEmptyTree.v(3KB)