Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series) Softcover reprint of edition by Bertot, Yves, Castéran, Pierre (2010) Paperback

by Yves Bertot

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.

Genres: Computer Science, Programming, Mathematics, Technical, Nonfiction

Paperback

First published June 24, 2004

Reviews

[Corey O'connor · Rating 5 out of 5]

Excellent! A good way to get started with formal proofs of correctness using Coq.

[Steve]

The first two chapters are just grab bags of random topics. I'll pick this up again later once I have a better understanding of how Coq is supposed to be used.