Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today. Learn more →
Top 23 coq Open-Source Projects
-
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 development of machine-checked proofs.
Project mention: Rosenpass – formally verified post-quantum WireGuard | news.ycombinator.com | 2023-02-28 -
Project mention: Rosenpass – formally verified post-quantum WireGuard | news.ycombinator.com | 2023-02-28
-
SonarLint
Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Project mention: Announcing Magmide Month! (proof language for/using Rust) | reddit.com/r/rust | 2023-02-28 -
-
Project mention: We Need Simpler Types (speculations on what can be improved in future type systems and on erasing the boundaries between types and values) | reddit.com/r/ProgrammingLanguages | 2022-09-14
https://github.com/ligurio/practical-fm Look for Coq, Agda, Idris, MS - F*.
-
Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.
-
awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [[email protected],@palmskog]
Project mention: Coq is one of the most fun and enjoyable programming languages I ever use. | reddit.com/r/math | 2023-03-13Coq has an awesome list by the community: https://github.com/coq-community/awesome-coq
-
InfluxDB
Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.
-
I've looked at both of these before, but neither of them fit the bill. Both are used for interactive execution of Coq programs from inside Neovim (I already use https://github.com/whonore/Coqtail for that purpose), but neither provides code completion. Nonetheless, thank you so much for your help. Much appreciated.
-
Project mention: What is a really cool thing you would want to write in Rust but don't have enough time, energy or bravery for? | reddit.com/r/rust | 2022-06-08
Coq of OCaml is a good example of how I want it to be for rust
-
-
You can check it out here: https://www.principiarewrite.com/
-
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
-
Project mention: Let's collect relatively new research programming languages in this thread | reddit.com/r/ProgrammingLanguages | 2022-11-15
Jasmin, late 2010s, a language designed to be lower-level than C and provide good low-level control for cryptographic code. Basically a new take on "C as a high-level assembly language", with formal semantics etc. I suspect that this design space is rather close to "a good language to use as a compiler backend", but I think this would require changes to Jasmin and no one is working on that as far as I know.
-
-
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
-
-
-
-
-
Project mention: Let's collect relatively new research programming languages in this thread | reddit.com/r/ProgrammingLanguages | 2022-11-15
https://github.com/koka-lang/koka Algebraic effects and reference counting. https://github.com/mit-plv/koika hardware description DSL for coq
-
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Project mention: Development Environment with guix shell for Coq Package | reddit.com/r/GUIX | 2022-08-21I want to run guix shell to create an environment with the dependencies required to build coq-library-undecidability.
-
next-700-module-systems
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
-
-
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-03-13.
coq related posts
- Inspiring OOP examples?
- Rosenpass – formally verified post-quantum WireGuard
- Any small/simple proof languages?
- What made you know that you wanted to pursue mathematics?
- Do you do any code in you research or graduate daily basis
- OpenAI might be training its AI technology to replace some software engineers, report says
- Is there a branch of math that studies the processes and skills of problem-solving themselves?
-
A note from our sponsor - SonarLint
www.sonarlint.org | 28 Mar 2023
Index
What are some of the best open-source coq projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | coq | 4,128 |
| 2 | CompCert | 1,571 |
| 3 | magmide | 750 |
| 4 | jscoq | 471 |
| 5 | practical-fm | 412 |
| 6 | proofs | 240 |
| 7 | awesome-coq | 215 |
| 8 | Coqtail | 205 |
| 9 | coq-of-ocaml | 202 |
| 10 | Coq-Equations | 195 |
| 11 | principia | 190 |
| 12 | verdi-raft | 165 |
| 13 | jasmin | 146 |
| 14 | fourcolor | 124 |
| 15 | kami | 122 |
| 16 | ttlite | 112 |
| 17 | coq-serapi | 109 |
| 18 | corn | 106 |
| 19 | toychain | 103 |
| 20 | koika | 102 |
| 21 | coq-library-undecidability | 93 |
| 22 | next-700-module-systems | 72 |
| 23 | vericert | 69 |
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com