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.

Types

HOL/Isabelle

[HOL Interactive Theorem Prover]

Coq (+ Cedille, + LTAC, ...)

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

Libraries

[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

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]

Resources

[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.

2022-11-15 b60caae
2022-11-01 d18a175
2022-11-01 f7dd172
2022-10-31 33a79e4
2022-10-27 750be1e
2021-09-22 52a677b
2021-09-21 7732812
2021-08-19 87d9551
2021-05-17 ef49552
2021-02-26 52257e0
2021-01-18 af0b1e0
2021-01-17 675fddc
2021-01-15 d1b02d2
2021-01-15 cccf2d4
2021-01-15 f2197ab
2021-01-15 5599273