coqprime
Prime number verifier
A proof assistant library for prime number certification using elliptic curves and Pocklington certificates
Prime numbers for Coq
37 stars
3 watching
18 forks
Language: Coq
last commit: 18 days ago
Linked from 2 awesome lists
coqelliptic-curvespocklington-certificateprime-numberstheorem-proving
Related projects:
Repository | Description | Stars |
---|---|---|
formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
thery/mathcomp-extra | A collection of reusable mathematical components and algorithms implemented in Coq | 5 |
hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |
mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
coq-polyhedra/coq-polyhedra | Formalizes convex polyhedra using theorem-proving in Coq | 22 |
thery/minirubik | Solves the mini Rubik 2x2 using theorem-proving in Coq | 4 |
uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |