Certified Programming with Dependent Types
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
-
Modeling and Proving in Computational Type Theory github.com
Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
-
Proof General proofgeneral.github.io
Generic interface for proof assistants based on the extensible, customizable text editor Emacs.
-
Coq tag on Theoretical Computer Science Stack Exchange cstheory.stackexchange.com
Coq › Resources > Books: “Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.”