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
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 |