Home » forums » LtU Forum

Print release of a textbook on the Coq proof assistant

For a few years now, I've been working on a textbook introducing the Coq proof assistant. It's been available freely online, and I'd like to announce now the availability of a print version from MIT Press. The site I've linked to includes links to order the book online.

Quick context on why LtUers might be interested in Coq: it supports machine checking of mathematical proofs, including in program verification and PL metatheory, some of the most popular applications of proof assistant technology.

Quick context on what distinguishes this book from other Coq resources: it focuses on the engineering techniques to develop large formal developments effectively. It turns out that there are some reusable lessons on how to write formal proofs so that they tend to continue to work even when theorem statements change over the courses of projects.

I'm grateful to MIT Press for agreeing to this experiment where I may continue distributing free versions of the book online.

By Adam Chlipala at 2013-12-13 18:57 | LtU Forum | previous forum topic | next forum topic | other blogs | 14235 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Dependently typed Red-Black trees

Proving in the large is certainly not a matter i would underestimate.
Unfortunately i am not as fluent Coq as i wish so i fear i won't tell you how great and appreciated your book is.

Instead i will revert to a nit-picking negative comment.
Is it me or you don't certify your Red-Black tree is ordered ?
• who cares it's balanced if it's not ordered ?
• higher-order nested data types can certify balanced 2-3 trees [1]

So, according to me, the added value of dependent types is you can prove the invariant that matters : the tree is ordered. Being balanced is just a bonus.

[1] Ralf Hinze. (1998). Numerical Representations as Higher-Order Nested Datatypes.

By Damien Guichard at Sat, 2013-12-14 05:59 | login or register to post comments

Right

An underappreciated advantage of formal verification in general is the chance to state and prove only those theorems that you decide are worth the effort. For that example in the book, I picked a particular subset of the claims that folks might want to see. Also not present is any kind of end-to-end proof of running time, though the balance invariant is an important ingredient for such a proof.

Perhaps you can think of a proof of the order invariant as an implicit exercise for the reader? :)

By Adam Chlipala at Sat, 2013-12-14 14:16 | login or register to post comments

Excellent

I've been teaching myself Coq for around a year and the online version of your textbook has been invaluable, especially for Coq-specific quirks (Ltac, Prop, syntactically-guarded recursion, etc.). Thanks a lot for writing it!

My only big hurdle with Coq so far has been its module system. I messed up a project quite badly while trying to make it modular, and only managed to salvage it with typeclasses. I know ML-style modules are meant to be the bee's knees, and Coq's first-class types makes the implementation particularly simple, but they still seem like boilerplate-factories to me :/

PS: A couple of other good references:

* http://www.cis.upenn.edu/~bcpierce/sf/
* http://poleiro.info/

By Chris Warburton at Sat, 2013-12-14 13:49 | login or register to post comments

Pierce's too

Indeed. I worked with Pierce's book when I was taking EECS 495 at Northwestern (listed in one of the classes using this text) and it was fascinating.

I'm greatly anticipating carving out some time for this text as well.

By Andy Gocke at Wed, 2013-12-18 23:15 | login or register to post comments

Watch the story telling

It's very readable partly because of the informal story telling approach you take with the subject. I'll probably come back to it more often.

But you're really close or over the border of what a number of scientists find acceptable in the presentation of material. Was this a very conscious decision? I like it but if you want to sell it abroad I would tune it down just one notch.

By marco at Wed, 2014-01-15 13:50 | login or register to post comments