Authors | |
Publisher | Springer, Berlin |
Year | |
Pages | 472 |
Version | hardback |
Language | English |
ISBN | 9783540208549 |
Categories | Mathematical logic |
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.
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions