The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Luke Palmer wrote:
> I'm going to be giving a presentation to a local functional 
> programming group about dependent types.  Does anyone know of a 
> potent, realistic example of (executable) code which is type safe, but 
> does not look type safe to most type systems?
>
> I have a few contrived examples in mind, but I was wondering if there 
> is a standard motivating example which is particularly poignant.

I like examples of type-preserving compilers.  You can find that kind of 
example and others, like a red-black tree implementation, in my draft 
textbook:
   http://adam.chlipala.net/cpdt/