Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free. Learn more →
Top 17 Coq coq Projects
-
Project mention: What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do? | reddit.com/r/compsci | 2022-09-15
Languages are often not verified in full, because doing so might be a tremendous task, and you often don't need to verify a whole language. Often just a subset of the features will allow you to do what you need to. One example of a partially verified C language: https://compcert.org/.
-
It's always a pleasant surprise to see people using Coq and other formal verification technology. We need more rigor in programming! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [1] (a variant of another useful tactic called `magic` which solve goals with existentials) which can automatically prove the theorem from the article.
[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
-
Scout APM
Truly a developer’s best friend. Scout APM is great for developers who want to find and fix performance issues in their applications. With Scout, we'll take care of the bugs so you can focus on building great things 🚀.
-
-
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
Raft has been manually verified which was the hurdle here that makes the result interesting:
-
-
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)
Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
-
talent.io
Download talent.io’s Tech Salary Report. Median salaries, most in-demand technologies, state of the remote work... all you need to know your worth on the market by tech recruitment platform talent.io
-
-
-
Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
-
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.
-
Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
-
PS: Obligatory plug for hs-to-coq.
-
Project mention: Rupicola: Relational Compilation for Performance-Critical Applications | reddit.com/r/Compilers | 2022-06-17
-
It's possible to do all that work still in Coq, so that the extracted code can directly be compiled into an executable. One way is to use the coq-simple-io library, which basically wraps the OCaml standard library (including functions for reading and writing files/stdin/stdout) as Coq axioms. For example, I did extraction that way in a previous iteration of AoC: https://github.com/Lysxia/advent-of-coq-2018/blob/master/sol/day01_1.v
-
Project mention: Aneris: Program logic for developing and verifying distributed systems | news.ycombinator.com | 2022-09-18
-
-
SonarQube
Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
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 2022-09-18.
Coq coq related posts
- What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?
- Development Environment with guix shell for Coq Package
- Formally Verifying Rust's Opaque Types
- New Coq tutorial
- Ask HN: Can the same individual accomplish more with programming than proofs?
- It took Russell and that other guy 360 pages to prove that 1+1=2. That's how rigorous math is.
- Which is the most abstract and bizzare book of mathematics you have ever came across?
-
A note from our sponsor - SonarQube
www.sonarqube.org | 26 Sep 2022
Index
What are some of the best open-source coq projects in Coq? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | CompCert | 1,455 |
| 2 | proofs | 228 |
| 3 | Coq-Equations | 186 |
| 4 | principia | 180 |
| 5 | verdi-raft | 163 |
| 6 | fourcolor | 122 |
| 7 | kami | 116 |
| 8 | corn | 104 |
| 9 | toychain | 98 |
| 10 | koika | 94 |
| 11 | coq-library-undecidability | 81 |
| 12 | vericert | 63 |
| 13 | hs-to-coq | 61 |
| 14 | rupicola | 42 |
| 15 | coq-simple-io | 24 |
| 16 | aneris | 21 |
| 17 | doubly-generic | 4 |
Find
remote jobs
at our new job board 99remotejobs.com.
There are
5 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.
Are you hiring? Post a new remote job listing for free.
Static code analysis for 29 languages.
Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
www.sonarqube.org