Course2007
Software Foundations
Benjamin C. Pierce et al.
Teaches logic, proof and programming-language theory by making you build the proofs in a proof assistant, where hand-waving is impossible.
link checked 17 Sept 2026FreeAdvanced
Computer Science · Formal Methods & Verification
Proof Assistants
A topic within Formal Methods & Verification, itself one of 9 topics in that field and part of Computer Science.
Reading on Proof Assistants
22 works
Book2013
Certified Programming with Dependent Types
Adam Chlipala
Argues Coq proofs should be built to survive changes in the theorem being proved, by leaning on dependent types and proof automation rather than long brittle hand-written tactic scripts.
FreeAdvanced