- Software Foundations
- Volume 1
- Volume 2
- Volume 3
- Volume 4: ongoing
- CPDT TODO: planned
Certified Programming with Dependent Types (CPDT), 2019, Adam Chlipala
- Readership: undergraduates, professionals
- Prerequisites:: Haskell programming, discrete mathematics, logic, Types and Programming Language(formal semantics and program verification)
- This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time.
- Topics: Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations.
- Free PDF Copy: http://adam.chlipala.net/cpdt/
Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions (Coq’Art), 2004th Edition, Yves Bertot, Pierre Castéran
- Readership: professionals
- A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software
- Resources: https://www.labri.fr/perso/casteran/CoqArt/
Mathematical Components, Assia Mahboubi, Enrico Tassi
- Readership: experienced Coq users
- Prerequisites:: Coq and Ssreflect programming
- An Introduction to the Mathematical Components library of Coq System.
- Free PDF Copy: https://math-comp.github.io/mcb/
Highlighted Topics and Papers