Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant /

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 w...

Full description

Bibliographic Details

Main Author:	Chlipala, Adam, 1981-
Format:	eBook
Language:	English
Published:	Cambridge, MA : The MIT Press, [2013]
Subjects:	Coq (Electronic resource) Automatic theorem proving > Computer programs. Computer programming. COMPUTER SCIENCE/General COMPUTER SCIENCE/Programming Languages Electronic books.
Online Access:	Connect to the full text of this electronic book