The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

My draft book Certified Programming with Dependent Types 
<http://adam.chlipala.net/cpdt/> is almost ready to enter the editorial 
process at MIT Press, in preparation for conventional publication.  I've 
finished my own tweaking and proofreading, and now I'm looking for a few 
more people to do thorough proofreading.

I'm probably not going to implement major changes, but I'm very eager to 
learn not just of typos but also of localized bits of explanation or 
coding choices that are bad.

I'll continue to be grateful for problems reported by anyone at any 
time, but I also hope to find a few (about 3?) "serious" proofreaders 
who are willing to commit to reading everything on a prearranged time 
scale (TBD), so I can pass on a schedule of my own to MIT Press.  It's 
the PDF version, not the HTML version, of CPDT that should be considered 
canonical for this purpose.

So, I'll appreciate e-mail from anyone who'd like to volunteer for this 
task.  Thanks in advance!

(It's probably worth saying what the book is about: It's an introduction 
to Coq, assuming nothing but experience with a typed functional language 
and undergraduate-level knowledge of discrete math and logic.  The style 
I follow is very different from what is found in any other resource out 
there, with a focus on dependent types and Ltac automation.)