Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev. Learn more →
Top 23 Coq coq Projects
-
Project mention: Can the language of proof assistants be used for general purpose programming? | news.ycombinator.com | 2023-10-27
Also a C compiler (https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible".
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.
-
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
Coq-HoTT (https://github.com/HoTT/Coq-HoTT)
agda-unimath (https://unimath.github.io/agda-unimath/)
cubical agda (https://github.com/agda/cubical)
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
-
Onboard AI
Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04https://github.com/magmide/magmide when
-
Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics? | /r/Coq | 2023-06-18
-
Project mention: A Taste of Coq and Correct Code by Construction | news.ycombinator.com | 2023-09-03
If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.
Any feedback is appreciated!
-
-
-
InfluxDB
Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.
-
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
-
Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics? | /r/Coq | 2023-06-18
-
Takes around 15 minutes on my machine.
[0] https://github.com/coq-community/fourcolor
[1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...
-
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
-
-
-
-
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
-
-
-
-
-
My point about a proof assistant language, let's just say Coq, is focused on pure, referentially transparent functions. There are no IORef like escape hatches required to make things work, although you could probably argue that stuff like this is still pure as, there are certainly escape hatches. Generally speaking, in proof assistants, the program can be self-contained, and is thus "pure".
-
-
regexp-Brzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
Project mention: Show HN: Regex Derivatives (Brzozowski Derivatives) | news.ycombinator.com | 2023-03-07Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coq-community/regexp-Brzozowski
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
NOTE:
The open source projects on this list are ordered by number of github stars.
The number of mentions indicates repo mentiontions in the last 12 Months or
since we started tracking (Dec 2020).
The latest post mention was on 2023-10-27.
Coq coq related posts
- Can the language of proof assistants be used for general purpose programming?
- A Taste of Coq and Correct Code by Construction
- Will Computers Redefine the Roots of Math?
- Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?
- Inspiring OOP examples?
- There is such thing called bugfree code.
- Proofs about Programs
-
A note from our sponsor - Onboard AI
getonboard.dev | 3 Dec 2023
Index
What are some of the best open-source coq projects in Coq? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | CompCert | 1,695 |
| 2 | UniMath | 876 |
| 3 | magmide | 784 |
| 4 | math-comp | 515 |
| 5 | proofs | 276 |
| 6 | Coq-Equations | 205 |
| 7 | jasmin | 189 |
| 8 | verdi-raft | 175 |
| 9 | analysis | 167 |
| 10 | fourcolor | 138 |
| 11 | kami | 132 |
| 12 | koika | 116 |
| 13 | toychain | 108 |
| 14 | corn | 108 |
| 15 | coq-library-undecidability | 98 |
| 16 | ConCert | 98 |
| 17 | vericert | 71 |
| 18 | hs-to-coq | 71 |
| 19 | rupicola | 46 |
| 20 | coq-simple-io | 27 |
| 21 | aneris | 27 |
| 22 | regexp-Brzozowski | 12 |
| 23 | doubly-generic | 4 |
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com