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

Libraries a neat representation of recursive and impure Coq programs function definitions for Coq metaprogramming

References index of coq tactics and their meanings coq and math? 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 "Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2020" formal reasoning about programs website denotational semantics of imperative language in the style of software foundations something to do with a coq plugin suite? verifcomp a great approach to coq through a sample z3 tutorial coqart: a textbook for learning more coq! Coq proofs for the informal programmer, supposedly