Certified Programming with Dependent Types A Pragmatic Introduction to the Coq Proof Assistant

A handbook to the Coq software for writing and checking mathematical proofs, with a practical engineering focus. 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...

Full description

Bibliographic Details
Format: eBook
Language:English
Published: Cambridge The MIT Press 2013
Series:The MIT Press
Subjects:
Online Access:Open Access: DOAB: description of the publication
Open Access: DOAB, download the publication