The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

I am looking for examples of practical uses of Coq to present in a 
class.  My big criteria are:

 * Applications outside of pure math are preferable.  I think of many 
developments in programming language semantics as "pure math" for this 
purpose.
 * I would like some small examples that could perhaps be presented in 
a 1.5 hour lecture, including some that are simple enough that they 
could be used early in the class to motivate why the audience should be 
interested in using proof assistants.
 * Some examples that use extraction would be good.

Can anyone point me to any good examples (with source code!) of this kind?

I would also be very interested to learn about any past successful 
doctoral-level classes focused on Coq.

Thanks!