From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2JGMsQT004221
	for <caml-list@sympa-roc.inria.fr>; Mon, 19 Mar 2012 17:22:54 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AoYXANhTZ0/RVdK0mGdsb2JhbABCjGuVM5MVBAECgQkIIgEBAQEBCAkNBxQnggoBAQQSAiwBGx4DDAYFCzsiAREBBQEcO4doC5xtCowSgnGEbT+IdAEFC4wOgUGDIgSIVo0Sjkk9hCg
X-IronPort-AV: E=Sophos;i="4.73,611,1325458800"; 
   d="scan'208";a="150179696"
Received: from mail-iy0-f180.google.com ([209.85.210.180])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Mar 2012 17:22:49 +0100
Received: by iage36 with SMTP id e36so15351265iag.39
        for <caml-list@yquem.inria.fr>; Mon, 19 Mar 2012 09:22:48 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :content-type;
        bh=sIvMUcone2j614Cc+oi+a1yCatNm/YHoR733CUjlgos=;
        b=vrG/3VHBbIZ9KpVzgMLIPZbDhrG8l05OKCxXeuD2StI3nijd3H2hV/ThPS8L2HnnG4
         lO+34aPdl0XC0Pkd4XRl8w3qH7/9oOHytSYB6oFaLV+ibxLbG14S6ZZF8VBxpTn0qzYf
         en5xxdSl/c9Ox8+NXdxu/6Q3G9IuSeMOAV37I4pgdbABmxTnYrOCVm38NW7iVkER4sqm
         xuc/sVIRs57RrJYTZPDeiYAm+H/VGA+P5NjiLu67cYDfmE4nYTxHPK27si/vJqrwxJ5i
         9+ryzWdE4qdhfADUrxNiOglCQEmltraVHLl3HrMAcWrkVOELp4cXHodRzyWVT7yVLgfo
         lH3w==
Received: by 10.50.184.228 with SMTP id ex4mr6479118igc.50.1332174167996; Mon,
 19 Mar 2012 09:22:47 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.43.132.200 with HTTP; Mon, 19 Mar 2012 09:22:26 -0700 (PDT)
In-Reply-To: <CAGrdgiVpG45Kgf2u0PHgDzH=yEOAMmydbXP-qsnLYC3MTzZSEw@mail.gmail.com>
References: <87aa3mawg1.fsf@frosties.localnet> <CAPFanBHcs4V2OHB1VjCvb+xizPbQ7NQfWH_GwAvfNfnQ1wtfLQ@mail.gmail.com>
 <CAGrdgiVpG45Kgf2u0PHgDzH=yEOAMmydbXP-qsnLYC3MTzZSEw@mail.gmail.com>
From: Raoul Duke <raould@gmail.com>
Date: Mon, 19 Mar 2012 09:22:26 -0700
Message-ID: <CAJ7XQb6Tq8Qa4K3_TQKKH+-MNnXoUBLS0T68LhzwdSBOxo=d3Q@mail.gmail.com>
To: caml-list@yquem.inria.fr
Content-Type: text/plain; charset=ISO-8859-1
Subject: Re: [Caml-list] Wanted: GADT examples: string length, counting module x

On Mon, Mar 19, 2012 at 9:13 AM, Jesper Louis Andersen
> If you want to play with dependent types, there are two ways which
> seem popular at the moment: Agda or Coq.

and some not popular ones...

http://www.ats-lang.org/

http://sandycat.info/blog/deptypes-shen/

et. al.