The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

On 13/08/14 20:01, Hugo Carvalho 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?

Maybe this:
│
└─ http://corn.cs.ru.nl//lib.html
   │
   └─ http://corn.cs.ru.nl//library/realcalc.html

?