coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/
- [Coq-Club] Examples of dependent type programming, Luke Palmer
- Re: [Coq-Club] Examples of dependent type programming, Adam Chlipala
- Re: [Coq-Club] Examples of dependent type programming, Frederic Blanqui
- Re: [Coq-Club] Examples of dependent type programming, Roland Zumkeller
Archive powered by MhonArc 2.6.16.