<P>A PRACTICAL INTRODUCTION TO THE DEVELOPMENT OF PROOFS AND CERTIFIED PROGRAMS USING COQ. </P> <P>AN INVALUABLE TOOL FOR RESEARCHERS, STUDENTS, AND ENGINEERS INTERESTED IN FORMAL METHODS AND THE DEVELOPMENT OF ZERO-FAULT SOFTWARE.</P>
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)