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

• Yazar: Chlipala, Adam (auth)
• Materyal Türü: Elektronik Kitap Bölümü
• Dil: İngilizce
• Baskı/Yayın Bilgisi: Cambridge The MIT Press 2013
• Seri Bilgileri: The MIT Press
• Konular: Mobile & handheld device programming / Apps programming; Computer programming / software engineering
• Online Erişim: 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...