Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Examples of dependent type programming

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Examples of dependent type programming


chronological Thread 
  • From: Adam Chlipala <adamc AT hcoop.net>
  • To: Luke Palmer <lrpalmer AT gmail.com>
  • Cc: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Examples of dependent type programming
  • Date: Tue, 14 Apr 2009 09:08:18 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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/





Archive powered by MhonArc 2.6.16.

Top of Page