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

• मुख्य लेखक: Chlipala, Adam (auth)
• स्वरूप: इलेक्ट्रोनिक पुस्तक अध्याय
• भाषा: अंग्रेज़ी
• प्रकाशित: Cambridge The MIT Press 2013
• श्रृंखला: The MIT Press
• विषय: Mobile & handheld device programming / Apps programming; Computer programming / software engineering
• ऑनलाइन पहुंच: DOAB: download the publication; DOAB: description of the publication

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