The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Dear Luke, CoLoR, http://color.inria.fr/, a Coq Library on Rewriting and 
termination, uses a lot of dependent types. You will find many such 
examples in it. They are for instance used for representing first-order 
algebraic terms with symbols of fixed arity 
(http://color.inria.fr/doc/CoLoR.Term.WithArity.ATerm.html), polynomials 
with multiples variables 
(http://color.inria.fr/doc/CoLoR.Util.Polynom.Polynom.html) or matrices 
on a (ordered) semi-ring 
(http://color.inria.fr/doc/CoLoR.Util.Matrix.Matrix.html). Many 
executable functions are defined on them. Best regards, Frederic.

Luke Palmer a écrit :
> 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.
>
> Thanks,
> Luke