Statistics for topic coq

RepositoryStats tracks 595,856 Github repositories, of these 87 are tagged with the coq topic. The most common primary language for repositories using this topic is Coq (52). Other languages include: OCaml (11)

Stargazers over time for topic coq

Most starred repositories for topic coq (view more)

coq
coq coq
660
4.9k
lgpl-2.1
103
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
coq dependent-types proof-assistant theorem-proving
Created 2011-02-17
44,672 commits to master branch, last one 22 hours ago
AbsInt
CompCert AbsInt
230
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,176 commits to master branch, last one 8 days ago
UniMath
UniMath UniMath
173
965
other
57
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
coq unimath coq-library foundations mathematics
Created 2014-03-01
10,270 commits to master branch, last one 2 days ago
Coq-zh
SF-zh Coq-zh
69
924
unknown
53
《软件基础》中译版 Software Foundations Chinese Translation
coq translation chinese-translation
Created 2018-04-04
127 commits to master branch, last one 2 years ago
magmide
magmide magmide
13
810
unknown
51
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
coq logic type-safety verification formal-methods dependent-types formal-verification systems-programming
Created 2020-08-21
195 commits to main branch, last one 8 months ago
jwiegley
category-theory jwiegley
71
761
bsd-3-clause
20
An axiom-free formalization of category theory in Coq for personal study and practical work
coq monad monoid functor category comonads cartesian categories profunctor construction category-theory profunctor-composition cartesian-closed-category
Created 2014-07-04
1,548 commits to master branch, last one 23 days ago

Trending repositories for topic coq (view more)

Last 3 days (new repositories)
no newly created repositories trending in the last 3 days
Last 3 days (absolute gain)
math-comp
math-comp/math-comp

Mathematical Components

596 (+2)
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

212 (+1)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,885 (+1)
lgpl-2.1
Last 3 days (relative gain)
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

212 (+0.5%)
math-comp
math-comp/math-comp

Mathematical Components

596 (+0.3%)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,885 (+0.0%)
lgpl-2.1
Last week (new repositories)
no newly created repositories trending in the last week
Last week (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,885 (+5)
lgpl-2.1
MetaCoq
MetaCoq/metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

397 (+4)
mit
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

212 (+2)
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

257 (+2)
mit
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

439 (+2)
agpl-3.0
Last week (relative gain)
MetaCoq
MetaCoq/metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

397 (+1%)
mit
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

212 (+1.0%)
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

257 (+0.8%)
mit
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

219 (+0.5%)
apache-2.0
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

439 (+0.5%)
agpl-3.0
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

219 (+20)
apache-2.0
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,885 (+20)
lgpl-2.1
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,905 (+14)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

439 (+13)
agpl-3.0
MetaCoq
MetaCoq/metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

397 (+13)
mit
Last month (relative gain)
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

219 (+10%)
apache-2.0
IBM
IBM/ACE-RISCV

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.

35 (+9%)
apache-2.0
sr-lab
sr-lab/coqpyt

Python client for coq-lsp

29 (+7%)
mit
WasmCert
WasmCert/WasmCert-Coq

A mechanisation of Wasm in Coq

101 (+5%)
mit
jaalonso
jaalonso/Lecturas_GLC

Readings on computational logic, interactive theorem proving and functional programming.

74 (+4%)
gpl-3.0
Last 12-months (new repositories)
no newly created repositories trending in the last 12 months
Last 12-months (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,885 (+420)
lgpl-2.1
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

439 (+364)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,905 (+204)
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

219 (+138)
apache-2.0
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

257 (+120)
mit
Last 12-months (relative gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

439 (+485%)
agpl-3.0
sr-lab
sr-lab/coqpyt

Python client for coq-lsp

29 (+314%)
mit
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

219 (+170%)
apache-2.0
IBM
IBM/ACE-RISCV

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.

35 (+150%)
apache-2.0
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

257 (+88%)
mit