![](/uploads/posts/2017-04/thumbs/1492528307_41rmeb-xqxl._sx383_bo1204203200_.jpg)
Автор: Adam Chlipala
Издательство: MIT Press
Год: 2013
Формат: PDF, EPUB
Размер: 11,8 Мб
Язык: английский / English
The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. 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.