Coq

Coq is a theorem prover that uses principles from type theory to provide formalizations of programs.

Libraries

https://github.com/DeepSpec/InteractionTrees a neat representation of recursive and impure Coq programs https://github.com/mattam82/Coq-Equations function definitions for Coq https://github.com/MetaCoq/metacoq metaprogramming

References

https://github.com/atharvashukla/coq-tactics-index index of coq tactics and their meanings https://github.com/UniMath/UniMath coq and math? https://github.com/codyroux/name-the-biggest-number proving the biggest number in coq constructively dmelcer9/coq-lunch-learn A formally verified high-level synthesis tool based on CompCert and written in Coq cs guy working on certicoq A collection of tools for writing technical documents that mix Coq code and prose. Coq to Cedille compiler written in Coq An axiom-free formalization of category theory in Coq for personal study and practical work Software Foundations https://github.com/hwayne/lets-prove-leftpad "Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2020" https://github.com/achlipala/frapapp formal reasoning about programs website denotational semantics of imperative language in the style of software foundations https://github.com/uwplse/pumpkin-pi something to do with a coq plugin suite? verifcomp https://www.reddit.com/r/Coq/comments/tzpb9/webbased_proofbypointing_frontend_to_coq/ https://news.ycombinator.com/item?id=26288749: a great approach to coq through a sample z3 tutorial coqart: a textbook for learning more coq! Coq proofs for the informal programmer, supposedly http://web.mit.edu/cpitcla/www/coq-rst/universe-polymorphism.html