Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series) Hardcover – 14 May 2004
- Choose from over 13,000 locations across the UK
- Prime members get unlimited deliveries at no additional cost
- Find your preferred location and add it to your address book
- Dispatch to this address when you check out
Customers who bought this item also bought
Customers also shopped for
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.
To get the free app, enter your mobile phone number.
Would you like to tell us about a lower price?
If you are a seller for this product, would you like to suggest updates through seller support?
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)
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.See all Product description
No customer reviews
|5 star (0%)|
|4 star (0%)|
|3 star (0%)|
|2 star (0%)|
|1 star (0%)|
Review this product
Most helpful customer reviews on Amazon.com
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. All the documentation information in this book, as well as a tutorial, are available on the inria website, but are not organized for learning or for beginners, autodidacts or self study as this fine text is. BUT the weaknesses of the book being dated are made up for on the website, which DOES have an 8.4 and above tutorial that you will understand easily after studying this book. Note that this is still the ONLY well written, BEGINNERS intro to Coq!
Coq USED to be (when this book was written) a research and development tool, and basically non-commercial. However, since that time, Coq has proven a number of practical theorems and has validated two new optimizing compilers (CompCert for C and one for Java). Because of this, Coq has suddenly become the "go to" solver/ proof engine for new languages that have to be validated and bulletproof at launch. I write domain specific languages for robotics, and although I don't achieve bulletproof in my compiles (which are at the VHDL/ circuit level), Coq is a wonderful "debugging" tool as well. It doesn't provide the level of code generation of Isabelle, but other than that is clearly the top proof assistant available.
Experience in OCaml is a plus, and Haskell is "almost" a necessity if you are developing a compiler to interact with the OCaml. Haskell's "lazy" access system also allows you to deluge the compiler with test junk that's only used if needed, so you don't have to worry about blowing out your memory when Coq decides to gallop. This book is for mature developers of new languages, and programmers that are interested in checking their code in a semi automated fashion, so obviously you need to know how to code-- well-- to use this book and these tools.
Library Picks reviews only for the benefit of Amazon shoppers and has nothing to do with Amazon, the authors, manufacturers or publishers of the items we review. We always buy the items we review for the sake of objectivity, and although we search for gems, are not shy about trashing an item if it's a waste of time or money for Amazon shoppers. If the reviewer identifies herself, her job or her field, it is only as a point of reference to help you gauge the background and any biases.
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 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. IMO Haskell is a better suited language for this system. YMMV ;-)
* For the most part you can follow along with the book in the coq toplevel. However, sometimes they omit definitions. Which caused me to struggle figuring out what I did wrong in transcribing the book. Only to discover I did nothing wrong and the book was skipping ahead a bit. By chapter 6 I don't recall this being an issue.
Note: I would rate this 4 stars but due to the 1 star review due to the poor kindle edition I decided to offset the rating a bit. The kindle edition really is poor, but I don't think it's fair to rate the entire book so low based off a single edition.