adam@518:
adam@518:
adam@518:
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
adamc@267:
adamc@267:
I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since short and automated proofs are the starting point, rather than an advanced topic.
adamc@267:
adam@518:
Interested in using this book in a course you're teaching? Please drop me a line!
adam@299:
adam@518:
A traditional hardcopy version is available from MIT Press, who have graciously agreed to allow distribution of free versions online indefinitely, minus the benefits of the Press' copy editing!
adam@518:
adam@518:
Buy a Copy in Print
adam@518:
adamc@39:
adamc@39:
adamc@39: