Statistics for language Coq

RepositoryStats tracks 597,388 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
230
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,178 commits to master branch, last one 2 days ago
gustavo-depaula
stalin-sort gustavo-depaula
178
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
523 commits to master branch, last one 20 days ago
HoTT
Coq-HoTT HoTT
194
1.3k
other
60
A Coq library for Homotopy Type Theory
type-theory homotopy-type-theory univalent-foundations
Created 2011-03-26
6,737 commits to master branch, last one 3 days ago
UniMath
UniMath UniMath
173
966
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 6 days 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 28 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)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,270 (+3)
coq-community
coq-community/fourcolor

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

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

442 (+2)
agpl-3.0
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+2)
mit-plv
mit-plv/koika

A core language for rule-based hardware design 🦑

146 (+1)
gpl-3.0
Last 3 days (relative gain)
coq-community
coq-community/fourcolor

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

180 (+2%)
mit-plv
mit-plv/koika

A core language for rule-based hardware design 🦑

146 (+0.7%)
gpl-3.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! ✈️ 🚀 ⚕️ 🏦

442 (+0.5%)
agpl-3.0
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+0.4%)
HoTT
HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

1,270 (+0.2%)
Last week (new repositories)
no newly created repositories trending in the last week
Last week (absolute gain)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,544 (+5)
mit
coq-community
coq-community/fourcolor

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

180 (+5)
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+4)
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

153 (+3)
mit
MetaCoq
MetaCoq/metacoq

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

400 (+3)
mit
Last week (relative gain)
coq-community
coq-community/fourcolor

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

180 (+3%)
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

153 (+2%)
mit
mit-plv
mit-plv/koika

A core language for rule-based hardware design 🦑

146 (+1%)
gpl-3.0
AU-COBRA
AU-COBRA/ConCert

A framework for smart contract verification in Coq

116 (+0.9%)
mit
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+0.8%)
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

153 (+30)
mit
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+21)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,544 (+16)
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! ✈️ 🚀 ⚕️ 🏦

442 (+15)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,908 (+14)
Last month (relative gain)
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

153 (+24%)
mit
TiarkRompf
TiarkRompf/reachability

No description

43 (+10%)
logsem
logsem/iris-tutorial

No description

29 (+7%)
mit
coq-community
coq-community/fourcolor

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

180 (+7%)
riscv
riscv/sail-riscv

Sail RISC-V model

486 (+5%)
Last 12-months (new repositories)
ccz181078
ccz181078/Coq-BB5

No description

160
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! ✈️ 🚀 ⚕️ 🏦

442 (+367)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,908 (+207)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,544 (+160)
mit
ccz181078
ccz181078/Coq-BB5

No description

160 (+159)
riscv
riscv/sail-riscv

Sail RISC-V model

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

442 (+489%)
agpl-3.0
logsem
logsem/iris-tutorial

No description

29 (+480%)
mit
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

153 (+248%)
mit
meithecatte
meithecatte/busycoq

Busy Beaver deciders backed by Coq proof

39 (+225%)
mit
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

39 (+105%)
mit