Statistics for language Coq

RepositoryStats tracks 585,902 Github repositories, of these 106 are reported to use a primary language of Coq.

Most starred repositories for language Coq (view more)

AbsInt
CompCert AbsInt
229
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,160 commits to master branch, last one 23 hours ago
gustavo-depaula
stalin-sort gustavo-depaula
177
1.5k
mit
10
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
stalin-sort hacktoberfest
Created 2018-10-30
521 commits to master branch, last one 9 days ago
HoTT
Coq-HoTT HoTT
193
1.3k
other
59
A Coq library for Homotopy Type Theory
type-theory homotopy-type-theory univalent-foundations
Created 2011-03-26
6,659 commits to master branch, last one 5 days ago
UniMath
UniMath UniMath
174
961
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,264 commits to master branch, last one 5 days ago
magmide
magmide magmide
13
812
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 7 months ago
jwiegley
category-theory jwiegley
70
755
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,545 commits to master branch, last one 4 days ago

Trending repositories for language Coq (view more)

Last 3 days (new repositories)
no newly created repositories trending in the last 3 days
Last 3 days (absolute gain)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,892 (+4)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,259 (+3)
mit-plv
mit-plv/fiat-crypto

Cryptographic Primitive Code Generation by Fiat

717 (+1)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,527 (+1)
mit
Last 3 days (relative gain)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,259 (+0.2%)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,892 (+0.2%)
mit-plv
mit-plv/fiat-crypto

Cryptographic Primitive Code Generation by Fiat

717 (+0.1%)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,527 (+0.1%)
mit
Last week (new repositories)
no newly created repositories trending in the last week
Last week (absolute gain)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,259 (+6)
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

168 (+5)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,892 (+5)
CertiCoq
CertiCoq/VeriFFI

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

38 (+3)
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! ✈️ 🚀 ⚕️ 🏦

424 (+2)
agpl-3.0
Last week (relative gain)
CertiCoq
CertiCoq/VeriFFI

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

38 (+9%)
mit
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

168 (+3%)
ccz181078
ccz181078/Coq-BB5

No description

158 (+0.6%)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,259 (+0.5%)
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! ✈️ 🚀 ⚕️ 🏦

424 (+0.5%)
agpl-3.0
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,892 (+17)
riscv
riscv/sail-riscv

Sail RISC-V model

462 (+16)
logsem
logsem/iris-tutorial

No description

26 (+13)
mit
MetaCoq
MetaCoq/metacoq

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

387 (+12)
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! ✈️ 🚀 ⚕️ 🏦

424 (+9)
agpl-3.0
Last month (relative gain)
logsem
logsem/iris-tutorial

No description

26 (+100%)
mit
IBM
IBM/FormalML

Formalization of Machine Learning Theory with Applications to Program Synthesis

74 (+9%)
apache-2.0
CertiCoq
CertiCoq/VeriFFI

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

38 (+9%)
mit
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

164 (+4%)
mit
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

168 (+4%)
Last 12-months (new repositories)
ccz181078
ccz181078/Coq-BB5

No description

158
formal-land
formal-land/coq-of-python

Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

30
mit
Last 12-months (absolute 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! ✈️ 🚀 ⚕️ 🏦

424 (+349)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,892 (+202)
ccz181078
ccz181078/Coq-BB5

No description

158 (+157)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,527 (+153)
mit
riscv
riscv/sail-riscv

Sail RISC-V model

462 (+120)
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! ✈️ 🚀 ⚕️ 🏦

424 (+465%)
agpl-3.0
logsem
logsem/iris-tutorial

No description

26 (+420%)
mit
meithecatte
meithecatte/busycoq

Busy Beaver deciders backed by Coq proof

39 (+225%)
mit
TiarkRompf
TiarkRompf/reachability

No description

38 (+124%)
CertiCoq
CertiCoq/VeriFFI

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

38 (+100%)
mit