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.
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.
From the reviews of the first edition:
This book serves as a Coq user manual, supporting both beginners and experts in the use of Coq and its underlying theory. ... Numerous exercises further enhance the utility as a learning aid. A supporting website provides downloadable source for all the examples and solutions to the exercises. As an introduction to Coq the book is self-contained ... . The book is also comprehensive ... . In summary, the book is an essential companion for every Coq user ... . (Valentin F. Goranko, Zentralblatt MATH, Vol. 1069, 2005)