Programs and Proofs
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.
- 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.
-
Formal Reasoning About Programs adam.chlipala.net
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
-
-
CoqInterval gitlab.inria.fr
Tactics for performing proofs of inequalities on expressions of real numbers.
-
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.
-
Certified Programming with Dependent Types adam.chlipala.net
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
Coq › Resources > Books: “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.”