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 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
The CompCert formally-verified C compilerProject mention: Rosenpass – formally verified post-quantum WireGuard | news.ycombinator.com | 2023-02-28
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.
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
A gently curated list of companies using verification formal methods in industryProject 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*.
My personal repository of formally verified mathematics.Project mention: Thoughts on proof assistants? | reddit.com/r/ProgrammingLanguages | 2022-12-13
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.
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-13
Coq has an awesome list by the community: https://github.com/coq-community/awesome-coq
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.
Interactive Coq Proofs in VimProject mention: Code completion for Coq. | reddit.com/r/neovim | 2022-09-05
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.
Formal verification for OCamlProject 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
A function definition package for Coq
The Principia Rewrite (by LogicalAtomist)Project mention: Principia Mathematica in modern notation. | reddit.com/r/math | 2022-07-21
You can check it out here: https://www.principiarewrite.com/
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Language for high-assurance and high-speed cryptography (by jasmin-lang)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.
Formal proof of the Four Color Theorem [[email protected]]
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
A SuperCompiler for Martin-Löf's Type Theory
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Coq Repository at Nijmegen [[email protected],@VincentSe]
A minimalistic blockchain consensus implemented and verified in Coq
A core language for rule-based hardware design 🦑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
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-21
I want to run guix shell to create an environment with the dependencies required to build coq-library-undecidability.
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
A formally verified high-level synthesis tool based on CompCert and written in Coq.
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
coq related posts
Inspiring OOP examples?
1 project | reddit.com/r/java | 12 Mar 2023
Rosenpass – formally verified post-quantum WireGuard
9 projects | news.ycombinator.com | 28 Feb 2023
Any small/simple proof languages?
2 projects | reddit.com/r/math | 28 Feb 2023
What made you know that you wanted to pursue mathematics?
1 project | reddit.com/r/math | 24 Feb 2023
Do you do any code in you research or graduate daily basis
1 project | reddit.com/r/math | 12 Feb 2023
OpenAI might be training its AI technology to replace some software engineers, report says
4 projects | reddit.com/r/programming | 28 Jan 2023
Is there a branch of math that studies the processes and skills of problem-solving themselves?
1 project | reddit.com/r/math | 22 Jan 2023
A note from our sponsor - SonarLint
www.sonarlint.org | 28 Mar 2023
What are some of the best open-source coq projects? This list will help you: