主题 · coq

coq

标记 coq 主题、收录中的开源项目，按星标数排序。

项目数

16

总星标数

17,684

平均星标数

1,105

占比

0.00%

常跟 coq 一起出现在同一个项目上的主题。

近期新秀

近 90 天内创建、标记 coq 主题的项目。

近 90 天内还没有新项目标记这个主题。

#1
rocq ↗@rocq-proverOCaml
Rocq Prover 是一个交互式定理证明器，或称为证明助手。它提供一种正式语言，用于撰写数学定义、可执行算法和定理，并提供一个半交互式开发机器检查证明的环境。
★ 5,562+4近 7 天星标变化
#2
CompCert ↗@AbsIntRocq Prover
CompCert 形式化验证的 C 语言编译器
★ 2,220+1近 7 天星标变化
#3
UniMath ↗@UniMathRocq Prover
这个 rocq 库旨在从单值化（univalent）观点将大量数学内容形式化。
★ 1,019+2近 7 天星标变化
#4
SF-zh ↗@Rocq-zhHTML
《软件基础》中文版
★ 974+0近 7 天星标变化
#5
aeneas ↗@AeneasVerifOCaml
适用于 Rust 程序的验证工具链
★ 948+17近 7 天星标变化
#6
magmide ↗@magmideRocq Prover
一种依赖类型证明语言，旨在让软件工程师能够编写可证明正确的裸机代码。
★ 835+0近 7 天星标变化
#7
category-theory ↗@jwiegleyRocq Prover
在 Coq 中进行个人研究与实务工作的范畴论（Category Theory）无公理形式化
★ 808+1近 7 天星标变化
#8
math-comp ↗@math-compRocq Prover
Mathematical Components
★ 696+1近 7 天星标变化
#9
Cosette ↗@uwdbLean
Cosette 是个自动化 SQL 求解器。
★ 686+0近 7 天星标变化
#10
verdi ↗@uwplseRocq Prover
在 Coq 中形式化验证分布式系统实现的框架
★ 625+0近 7 天星标变化
#11
practical-fm ↗@ligurio
一份精心整理在业界使用形式化验证方法的公司清单
★ 610+1近 7 天星标变化
#12
PG ↗@ProofGeneralEmacs Lisp
此仓库为 Proof General 的新家。
★ 558+2近 7 天星标变化
#13
rocq-tricks ↗@rocq-communityCoq
你希望 Coq 手册早点告诉你的技巧 [维护者=@tchajed]
★ 552+0近 7 天星标变化
#14
metarocq ↗@MetaRocqRocq Prover
元编程、验证过的元理论，以及在 Rocq 中实现 Rocq。
★ 550+1近 7 天星标变化
#15
jscoq ↗@jscoqTypeScript
Coq 的 JavaScript 移植版——在浏览器中运行 Coq
★ 547+0近 7 天星标变化
#16
VST ↗@PrincetonUniversityRocq Prover
验证软件工具链 (Verified Software Toolchain)。
★ 508+1近 7 天星标变化

← 返回主题列表