The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

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?