Theorem Provers

Theorem provers are automated or semi-automated tools for composing proofs about statements or programs, allowing one to express their thoughts

[]It's one of the biggest one of these...

[]Huge motivation for the funding and introduction of formal methods for chip development.



[HOL Interactive Theorem Prover]

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

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.

[]a neat representation of recursive and impure Coq programs

[]function definitions for Coq



[]index of coq tactics and their meanings

[]coq and math?

[]proving the biggest number in coq constructively


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



[]a great approach to coq through a sample z3 tutorial

[coqart]: a textbook for learning more coq!

[Coq proofs for the informal programmer, supposedly]



[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