๐Ÿ“• subnode [[@jakeisnt/coq]] in ๐Ÿ“š node [[coq]]
๐Ÿ“• text contributed by @jakeisnt ๐Ÿ”—

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


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


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/ 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

Receiving pushes... (requires JavaScript)
Loading context... (requires JavaScript)
๐Ÿ“– stoas (collaborative spaces) for [[@jakeisnt/coq]]