coqprime

Prime number verifier

A proof assistant library for prime number certification using elliptic curves and Pocklington certificates

Prime numbers for Coq

GitHub

37 stars
3 watching
18 forks
Language: Coq
last commit: 18 days ago
Linked from 2 awesome lists

coqelliptic-curvespocklington-certificateprime-numberstheorem-proving

Backlinks from these awesome lists:

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