GoogleDDGWikipediaTwitterGithubEALWWorld ProblemsPubPub

Coq is a theorem proverthat 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 languagein 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/