coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Examples of dependent type programming

From: Luke Palmer <lrpalmer AT gmail.com>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Examples of dependent type programming
Date: Tue, 14 Apr 2009 06:59:30 -0600
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=w9YGm3s4GbWWcBDWBLrMSb8E0cl3KN3u1scq0ImCb4OqXmkB2GGYlMsMfkbyeP0phE 1cuexbXjbJoL9jeSYzasIl7cuRyAMv7zOvik+XZs2IozYDJGZwMLkGt8GrnaghLx1ISx F/KEauLCRpDy/Ct+66mQTFjPpW3X69EN7J7+M=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[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