Theorem Provers
Theorem provers are automated or semi-automated tools for composing proofs about statements or programs, allowing one to express their thoughts
[https://github.com/hwayne/awesome-cold-showers:]It's one of the biggest one of these...
[https://en.wikipedia.org/wiki/Pentium_FDIV_bug:]Huge motivation for
the funding and introduction of formal methods for chip development.
Coq is a {theorem prover} that uses
principles from type theory to provide formalizations of programs.
[Logitext]: A
theorem prover built on Haskell and Ur/Web. Worth reading and learning about -
or at least inspecting the source code. Not sure if UrWeb is worth it but it
looks fun to poke around with.
[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
[A formally verified high-level synthesis tool based on CompCert and written in
Coq]
[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]
[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?
[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]
[Software
Foundations]: Learn about the foundations of software through
exploring the proof assistant, Coq.
[Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF)
with...]
["A
Little Taste of Dependent Types" by David Christiansen - YouTube]
: Goes along with the "little typer" book!
[My hobby:
proof engineering | Stephan Boyer]: A writeup from an AirBnB software
engineer about proving things in Coq for fun; this helps Stephan explore ideas
and justify ides in types, logic, and algorithms; proving ideas is a tool for
thinking about them.
Types
HOL/Isabelle
Coq (+ Cedille, + LTAC, ...)
Libraries
References
Resources