coq algs:Coq中经过正式验证的算法和数据结构:概念和技术 源码

辅酶 您好。 该存储库包含一些随机的Coq代码,其中大多数与纯功能算法和数据结构有关。 它还包含我的硕士论文,也与算法有关。 开发的结构如下: RCCBase.v包含一些基本策略和辅助材料。 ADT /包含抽象数据类型的接口,例如队列,优先级队列,集合,有限映射等。 Data /包含基本归纳数据类型的实现,其中大多数是树。 这些基本树然后用于实现数据结构。 DS /包含数据结构,例如BST,堆,序列等。 记忆/是记忆功能的la脚尝试。 没什么值得一看的。 反射/在反射证明上有一些代码,也很la脚。 Sorting /包含各种排序算法的实现。 结构/具有排序和反射所需的代数和阶理论结构的实现。 垃圾/是垃圾。 甚至都不要看。 已完成 Structures /包含LinDec (可确定的线性顺序的实现),可用于大多数排序算法,以及一些词条和功能强大的自动化策略dec(称为d