Certified Programming with Dependent Types
A Pragmatic Introduction to the Coq Proof Assistant
Book Details
| Author | Adam Chlipala |
| Publisher | MIT Press |
| Published | 2019 |
| Edition | 1st |
| Paperback | 368 pages |
| Language | English |
| ISBN-13 | 9780262545747, 9780262026659 |
| ISBN-10 | 0262545748, 0262026651 |
| License | Creative Commons Attribution-NonCommercial-NoDerivatives |
Book Description
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 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.
Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers will acquire the necessary skills to reimplement these tactics in other settings by the end of the book.
This book is available under a Creative Commons Attribution-NonCommercial-NoDerivatives license (CC BY-NC-ND), which means that you are free to copy and distribute it, as long as you attribute the source, don't use it commercially, and don't create modified versions.
If you enjoyed the book and would like to support the author, you can purchase a printed copy (hardcover or paperback) from official retailers.
Download and Read Links
Share this Book
[localhost]# find . -name "*Similar_Books*"
Introduction to Data Science
Introduction to Data Science: Data Analysis and Prediction Algorithms with R introduces concepts and skills that can help you tackle real-world data analysis challenges. It covers concepts from probability, statistical inference, linear regression, and machine learning. It also helps you develop skills such as R programming, data wrangling, data vi
Rethinking the Internet of Things
Apress is proud to announce that Rethinking the Internet of Things was a 2014 Jolt Award Finalist, the highest honor for a programming book. And the amazing part is that there is no code in the book. Over the next decade, most devices connected to the Internet will not be used by people in the familiar way that personal computers, tablets and smart
An Introduction to C & GUI Programming, 2nd Edition
Freshly updated for GTK3, the 2nd edition of An Introduction to C & GUI Programming will teach you all you need to know to write simple programs in C and start creating GUIs, even if you're an absolute beginner. The first half of the book is an introduction to C, and covers the basics of writing simple command-line programs. The second half shows h
How To Code in Go
This book is designed to introduce you to writing programs with the Go programming language. You'll learn how to write useful tools and applications that can run on remote servers, or local Windows, macOS, and Linux systems for development. The topics that it covers include how to: - Install and set up a local Go development environment on Windows,
The Real-Time APIs
Application Programming Interfaces (APIs) are seemingly everywhere. Thanks to the popularity of web-based products, cloud-based X-as-a-service offerings, and IoT, it is becoming increasingly important for engineers to understand all aspects of APIs, from design, to building, to operation. Research shows that there is increasing demand for near real
Programming for Computations - MATLAB/Octave
This book presents computer programming as a key method for solving mathematical problems. There are two versions of the book, one for MATLAB and one for Python. The book was inspired by the Springer book TCSE 6: A Primer on Scientific Programming with Python (by Langtangen), but the style is more accessible and concise, in keeping with the needs o