Theorem provers are automated or semi-automated tools for composingproofs about statements or programs, allowing one to express theirthoughts It's one of thebiggest one of these… Huge motivation forthe funding and introduction of formal methods for chip development.



HOL Interactive Theorem Prover

Coq (+ Cedille, + LTAC, …)

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


Logitext: A theorem prover built onHaskell and Ur/Web. Worth reading and learning about - or at leastinspecting the source code. Not sure if UrWeb is worth it but it looksfun to poke around with. neat representation of recursive and impure Coq programs function definitions for Coq metaprogramming

References index of coqtactics and their meanings coq andmath? proving thebiggest number in coq constructivelydmelcer9/coq-lunch-learnA formally verified high-level synthesis tool based on CompCert andwritten inCoqcs guy working on certicoq Acollection of tools for writing technical documents that mix Coq codeand prose. Coq to Cedillecompiler written in Coq Anaxiom-free formalization of category theory in Coq for personal studyand practical workSoftware Foundations "Problem Sets for MIT6.822 Formal Reasoning About Programs, Spring2020" formal reasoning about programswebsite denotational semantics of imperativelanguage in the styleof software foundations somethingto do with a coq plugin suite? verifcomp a great approach to coqthrough a sample z3 tutorialcoqart:a textbook for learning more coq! Coq proofs for the informalprogrammer, supposedly


Software Foundations:Learn about the foundations of software through exploring the proofassistant, Coq. Introduction to Homotopy Type Theory and UnivalentFoundations (HoTT/UF)with…"A Little Taste of Dependent Types" by David Christiansen -YouTube: Goesalong with the "little typer" book! My hobby: proof engineering \|StephanBoyer:A writeup from an AirBnB software engineer about proving things in Coqfor fun; this helps Stephan explore ideas and justify ides in types,logic, and algorithms; proving ideas is a tool for thinking about them.