很棒的 精选的Coq框架,库和软件的精选清单。 经过正式认证的CompCert C编译器 此coq库旨在使用单价观点形式化大量数学。 -Coq中用于个人学习和实践工作的范畴论的无公理形式化 用于正式验证Coq中的分布式系统实现的框架 数学组件 您希望Coq手册告诉您的技巧 将Haskell源代码转换为Coq源代码 -Vellvm(已验证LLVM)coq开发。 - 对Coq中单价数学基础的原始发展 -FSCQ是在Coq中编写并证明的经过认证的文件系统 使用Coq证明助手进行定理证明的学习环境 -Coq中的元编程 -Coq的基于属性的随机测试插件 具有经验证的参考解释器的ECMA