Programming Books C Java PHP Python Learn more Browse Programming Books
Buy New
$79.10
Qty:1
  • List Price: $109.00
  • Save: $29.90 (27%)
Only 3 left in stock (more on the way).
Ships from and sold by Amazon.com.
Gift-wrap available.
Add to Cart
Want it Friday, April 18? Order within and choose Two-Day Shipping at checkout. Details
Trade in your item
Get a $18.53
Gift Card.
Have one to sell?
Flip to back Flip to front
Listen Playing... Paused   You're listening to a sample of the Audible audio edition.
Learn more

Interactive Theorem Proving and Program Development Hardcover

ISBN-13: 978-3540208549 ISBN-10: 3540208542 Edition: 2004th

See all 3 formats and editions Hide other formats and editions
Amazon Price New from Used from Collectible from
Kindle
"Please retry"
Hardcover
"Please retry"
$79.10
$79.10 $78.99

Free%20Two-Day%20Shipping%20for%20College%20Students%20with%20Amazon%20Student



NO_CONTENT_IN_FEATURE

Shop the new tech.book(store)
New! Introducing the tech.book(store), a hub for Software Developers and Architects, Networking Administrators, TPMs, and other technology professionals to find highly-rated and highly-relevant career resources. Shop books on programming and big data, or read this week's blog posts by authors and thought-leaders in the tech industry. > Shop now

Product Details

  • Series: Texts in Theoretical Computer Science. An EATCS Series
  • Hardcover: 500 pages
  • Publisher: Springer; 2004 edition (May 14, 2004)
  • Language: English
  • ISBN-10: 3540208542
  • ISBN-13: 978-3540208549
  • Product Dimensions: 9.4 x 6.5 x 1.3 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,343,866 in Books (See Top 100 in Books)

Editorial Reviews

Review

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.


More About the Author

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

Customer Reviews

3.7 out of 5 stars
5 star
2
4 star
0
3 star
0
2 star
0
1 star
1
See all 3 customer reviews
Share your thoughts with other customers

Most Helpful Customer Reviews

4 of 4 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
1 of 2 people found the following review helpful By Let's Compare Options 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
10 of 24 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

Product Images from Customers

Search
ARRAY(0xa3a2c57c)

What Other Items Do Customers Buy After Viewing This Item?