Enter your mobile number or email address below and we'll send you a link to download the free Kindle App. Then you can start reading Kindle books on your smartphone, tablet, or computer - no Kindle device required.

  • Apple
  • Android
  • Windows Phone
  • Android

To get the free app, enter your mobile phone number.

Interactive Theorem Proving and Program Development 2004th Edition

3.7 out of 5 stars 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.
Trade in your item
Get a $2.00
Gift Card.
Have one to sell? Sell on Amazon
Buy used On clicking this link, a new layer will be open
$56.78 On clicking this link, a new layer will be open
Buy new On clicking this link, a new layer will be open
$109.00 On clicking this link, a new layer will be open
More Buying Choices
34 New from $70.03 29 Used from $52.29
Free Two-Day Shipping for College Students with Prime Student Free%20Two-Day%20Shipping%20for%20College%20Students%20with%20Amazon%20Student

Windows 10 For Dummies Video Training
Get up to speed with Windows 10 with this video training course from For Dummies. Learn more.
$109.00 FREE Shipping. Only 4 left in stock (more on the way). Ships from and sold by Amazon.com. Gift-wrap available.
click to open popover

Frequently Bought Together

  • Interactive Theorem Proving and Program Development
  • +
  • Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (MIT Press)
  • +
  • Program Logics for Certified Compilers
Total price: $254.68
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.

The latest book club pick from Oprah
"The Underground Railroad" by Colson Whitehead is a magnificent novel chronicling a young slave's adventures as she makes a desperate bid for freedom in the antebellum South. See more

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: #1,472,685 in Books (See Top 100 in Books)

Customer Reviews

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

Top Customer Reviews

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 7 people found this helpful. Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback.
Sorry, we failed to record your vote. Please try again
Report abuse
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 6 people found this helpful. Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback.
Sorry, we failed to record your vote. Please try again
Report abuse
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 12 people found this helpful. Was this review helpful to you? Yes No Sending feedback...
Thank you for your feedback.
Sorry, we failed to record your vote. Please try again
Report abuse

Set up an Amazon Giveaway

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