Statistics for language Coq

RepositoryStats tracks 579,556 Github repositories, of these 105 are reported to use a primary language of Coq.

Most starred repositories for language Coq (view more)

AbsInt
CompCert AbsInt
228
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,156 commits to master branch, last one 7 days ago
gustavo-depaula
stalin-sort gustavo-depaula
175
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
516 commits to master branch, last one 20 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,592 commits to master branch, last one 2 days ago
UniMath
UniMath UniMath
174
960
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,260 commits to master branch, last one a day 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
69
752
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,541 commits to master branch, last one about a month 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)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,523 (+5)
mit
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

162 (+1)
mit
math-comp
math-comp/math-comp

Mathematical Components

586 (+1)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+1)
Last 3 days (relative gain)
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

162 (+0.6%)
mit
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,523 (+0.3%)
mit
math-comp
math-comp/math-comp

Mathematical Components

586 (+0.2%)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+0.1%)
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,523 (+5)
mit
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

162 (+1)
mit
math-comp
math-comp/math-comp

Mathematical Components

586 (+1)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+1)
Last week (relative gain)
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

162 (+0.6%)
mit
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,523 (+0.3%)
mit
math-comp
math-comp/math-comp

Mathematical Components

586 (+0.2%)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+0.1%)
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
riscv
riscv/sail-riscv

Sail RISC-V model

456 (+20)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+16)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,523 (+16)
mit
logsem
logsem/iris-tutorial

No description

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

419 (+14)
agpl-3.0
Last month (relative gain)
logsem
logsem/iris-tutorial

No description

25 (+150%)
mit
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

162 (+6%)
mit
uds-psl
uds-psl/coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.

110 (+5%)
mpl-2.0
coq-community
coq-community/fav-ssr

Functional Algorithms Verified in SSReflect [maintainer=@clayrat]

45 (+5%)
mit
riscv
riscv/sail-riscv

Sail RISC-V model

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

No description

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

419 (+347)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,881 (+195)
gustavo-depaula
gustavo-depaula/stalin-sort

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

1,523 (+162)
mit
ccz181078
ccz181078/Coq-BB5

No description

156 (+155)
riscv
riscv/sail-riscv

Sail RISC-V model

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

419 (+482%)
agpl-3.0
logsem
logsem/iris-tutorial

No description

25 (+400%)
mit
meithecatte
meithecatte/busycoq

Busy Beaver deciders backed by Coq proof

39 (+225%)
mit
TiarkRompf
TiarkRompf/reachability

No description

37 (+118%)
mit-frap
mit-frap/spring23

Problem Sets for MIT 6.512 Formal Reasoning About Programs, Spring 2023

28 (+65%)