The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, Hugo.

The Homotopy Type Theory book is a nice example.  It can be found here:

http://homotopytypetheory.org/book/

A large portion of the book was formalized as it was written.

Very best,

.\ Harley

On Aug 13, 2014, at 3:01 PM, Hugo Carvalho <hugoccomp AT gmail.com> wrote:

I'm curious to know if there have been efforts towards a full formalization of any textbook. I do know of the few books that have accompanying Coq code (Software Foundations, CPDT, Coq'Art). but i'm more interested in knowing if there is a textbook that was given a formalization after-the-fact (but then again, a textbook written from the ground-up with formalization in mind is also an interesting project, even if for different reasons).

It seems to me that, outside of "pure Computer Science" topics (such as programming, languages, algorithms), the most adequate topic for such a textbook would be math; logic and discrete math, specially, but other math topics also seem plausible.

Does the Club know of any pointers in this area?