Industrial-Sized Deals TextBTS15 Shop Women's Handbags Learn more nav_sap_plcc_6M_fly_beacon Melanie Martinez $5 Off Fire TV Stick Labor Day Sale in Wine Shop Popular Services pivdl pivdl pivdl  Amazon Echo Starting at $99 Kindle Voyage Nintendo Digital Games Shop Back to School with Amazon Back to School with Amazon Outdoor Recreation STEM Toys & Games
Interactive Theorem Proving and Program Development: Coq'... and over one million other books are available for Amazon Kindle. Learn more

Interactive Theorem Proving and Program Development 2004th Edition

3 customer reviews
ISBN-13: 978-3540208549
ISBN-10: 3540208542
Why is ISBN important?
This bar-code number lets you verify that you're getting exactly the right version or edition of a book. The 13-digit and 10-digit formats both work.
Scan an ISBN with your phone
Use the Amazon App to scan ISBNs and compare prices.
Sell yours for a Gift Card
We'll buy it for $34.32
Learn More
Trade in now
Have one to sell? Sell on Amazon
Buy used
Buy new
More Buying Choices
38 New from $68.66 18 Used from $69.20
Free Two-Day Shipping for College Students with Amazon Student Free%20Two-Day%20Shipping%20for%20College%20Students%20with%20Amazon%20Student

InterDesign Brand Store Awareness Rent Textbooks
$91.63 FREE Shipping. In Stock. Ships from and sold by Gift-wrap available.

Frequently Bought Together

Interactive Theorem Proving and Program Development + Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant + Program Logics for Certified Compilers
Price for all three: $218.42

Buy the selected items together

Editorial Reviews


From the reviews of the first edition:

"This book serves as a Coq user manual, supporting both beginners and experts in the use of Coq and its underlying theory. … Numerous exercises further enhance the utility as a learning aid. A supporting website provides downloadable source for all the examples and solutions to the exercises. As an introduction to Coq the book is self-contained … . The book is also comprehensive … . In summary, the book is an essential companion for every Coq user … ." (Valentin F. Goranko, Zentralblatt MATH, Vol. 1069, 2005)

From the Back Cover

Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory.

This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.


Best Books of the Month
Best Books of the Month
Want to know our Editors' picks for the best books of the month? Browse Best Books of the Month, featuring our favorite new books in more than a dozen categories.

Product Details

  • Series: Texts in Theoretical Computer Science. An EATCS Series
  • Hardcover: 500 pages
  • Publisher: Springer; 2004 edition (June 24, 2004)
  • Language: English
  • ISBN-10: 3540208542
  • ISBN-13: 978-3540208549
  • Product Dimensions: 6.1 x 1.1 x 9.2 inches
  • Shipping Weight: 1.8 pounds (View shipping rates and policies)
  • Average Customer Review: 3.7 out of 5 stars  See all reviews (3 customer reviews)
  • Amazon Best Sellers Rank: #729,650 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

5 star
4 star
3 star
2 star
1 star
See all 3 customer reviews
Share your thoughts with other customers

Most Helpful Customer Reviews

7 of 7 people found the following review helpful By C. OCONNOR on December 26, 2012
Format: Paperback
I tried to learn Coq with no success before I got this book. I'm not in school. I'm just a working professional with strong Haskell skills. I'm learning this on my own. Which makes this material, probably, more difficult for me than for a student or grad student who can work with a teacher and other students as they learn.

This book really was the only successful approach I've found for learning Coq on my own. The beginning chapters do a great job at slowly introducing the concepts that underly Coq. The typing rules start out overly simple, just to get you started. Then they revisit the typing rules as new concepts are added. Which, even outside of Coq, is very useful. The explanations at each point are very clear. By the end of chapter 6 I was comfortable with the concepts that underly Coq's type system. The later chapters go over more advanced topics which included program extraction. Program extraction was really the point at which I went "Ah ha!" and started to understand how I could apply Coq to practical applications. After several unsuccessful attempts this really was a great achievement for me. If I knew I would have a good understanding of these concepts for only a ~100$ investment I would have bought this book when it first came out. That would have saved me a lot of unnecessary struggles.

The downsides:

* The book is slightly out of date. Coq 8.4 (the latest as of the writing of this review) is more capable than the Coq 8.1 (?) the book was written against. There are several instances where the book explicitly says to try something to observe Coq failing. However, Coq 8.4 would rarely fail as the book described. Which is nice in a way but can be confusing. After chapter 5 this occurs less and less.
* The book references O'Caml more than Haskell.
Read more ›
Comment Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback. If this review is inappropriate, please let us know.
Sorry, we failed to record your vote. Please try again
6 of 8 people found the following review helpful By Let's Compare Options Preptorial TOP 500 REVIEWER on September 2, 2013
Format: Hardcover Verified Purchase
Coq is a semi automated, interactive theorem prover (colloquially a proof assistant) that works with both math and programming expressions. It's coded in OCaml, it's a generally functional paradigm, and its typing discipline is static and strong. Typing in developing new programming languages is about ontology and taxonomy (how classes, objects, organization, methods, classifications and much more are set up and separated), NOT typing on a keyboard. Typing is the way programs check for consistency, which is a kind of error detection and/or avoidance, and thus VERY relevant to Coq.

Speaking of typing, you MUST understand typing to use this book. Any book on developing new programming languages (and some on DSLs) will cover typing if written after the 90's (/during oop season), but if you have cash to burn, Ben Pierce is the go to guy on that: Types and Programming Languages, available used for about $30+ US on Amazon.

Both the 2004 and 2005 hardcover and paperback of this book are the same, so shop for the best price. These books cover several releases back, and the stable releases from 2013 and up are not backward compatible. The software is freely available at coq dot inria dot fr, and you will need it to use this book. Ssreflect, a significant new set of tools for Coq, also is freely available and is not covered except on the website. (You CANNOT get this book on a website, or free, the documentation does NOT include this book's pedagogy).

This book is a MUST as a great general intro to how, where and why to use Coq.
Read more ›
Comment Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback. If this review is inappropriate, please let us know.
Sorry, we failed to record your vote. Please try again
11 of 28 people found the following review helpful By Christoph Seufert on June 20, 2011
Format: Kindle Edition Verified Purchase
Contentwise the Book is great. BUT: The Kindle Edition looks like the book has been scanned and is nearly unreadable. If you don't believe it get the preview. If it would be possible i would claim ma money back. I STRONGLY recommend to get one of the paper-editions.
5 Comments Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback. If this review is inappropriate, please let us know.
Sorry, we failed to record your vote. Please try again

Set up an Amazon Giveaway

Amazon Giveaway allows you to run promotional giveaways in order to create buzz, reward your audience, and attract new followers and customers. Learn more
Interactive Theorem Proving and Program Development
This item: Interactive Theorem Proving and Program Development
Price: $91.63
Ships from and sold by

Want to discover more products? Check out these pages to see more: software engineering, software development, software testing