Coq是一个形式化证明管理系统。它提供了一种形式化语言来编写 数学定义、可执行算法和定理的...
数学组件是一个使用Coq证明助手开发的形式化数学的资源库。 的形式化数学资料库。这个项目...
数学是一个知识领域，包括诸如数字、公式和相关结构、形状和它们所包含的空间，以及数量及其变化...
在教育领域，教程是一种传授知识的方法，可作为学习过程的一部分。与书本或讲座相比，教程的互动...
C语言是由贝尔实验室的丹尼斯-里奇设计的一种编程语言。C语言使用非常广泛，简单明了，可以编...
编译器是将高层次（更适合人类阅读）的编程语言翻译成低层次语言（如机器码）的软件。处理器执行...
经CompCert正式验证的C语言编译器
这个coq库的目的是用单价的观点来形式化大量的数学作品。
一种依赖类型的证明语言，旨在为工作中的软件工程师提供可证明正确的裸机代码。
用于个人学习和实际工作的Coq范畴理论的无公理形式化
用Coq正式验证分布式系统实现的框架
数学成分
数学成分顺应分析库
关于通过SSReflect在Coq中证明/编程的短期课程的讲义。
四色定理的正式证明 [维护者=@ybertot]
分布式分离逻辑：分布式协议及其在Coq中的实现的复合验证框架
Coq中的单体效应和等式推理
Coq有效代数库 [维护者=@CohenCyril,@proux01] 。
信息理论和线性纠错码的Coq形式化