Proofs and Reliable Programming using Coq

team.inria.frsite

Introduction to developing and verifying programs with Coq.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Programs and Proofs ilyasergey.net

   site category #coq link ↗

   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.

2. ▲
   Certified Programming with Dependent Types adam.chlipala.net

   site category #coq link ↗

   Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.

3. ▲
   Mike Nahas's Coq Tutorial mdnahas.github.io

   site category #coq link ↗

   Basics of using Coq to write formal proofs.

4. ▲
   Official Coq standard library coq.inria.fr

   site category #coq link ↗
   
5. ▲
   Volume 3: Verified Functional Algorithms softwarefoundations.cis.upenn.edu

   site category #coq link ↗

   Demonstration of how a variety of fundamental data structures can be specified and verified.

6. ▲
   Formal Reasoning About Programs adam.chlipala.net

   site category #coq link ↗

   Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.

Coq › Resources > Course Material: “Introduction to developing and verifying programs with Coq.”