coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Programming language shootout for Coq?

From: Bas Spitters <spitters AT cs.ru.nl>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Programming language shootout for Coq?
Date: Tue, 2 Mar 2010 09:25:18 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=vKFH6TK92pBJRTt1512XzJM/Pvn2y/QGcbW94F8Hk/ixhn6pVBt22RWtxjnKzAVJrq CtyFr26dzQvnzqbAnESQokP00NulxO+AHA9X6tFGUX0g9Gu3uHQKb8twi/MJJvwXGsQz xJ2L/9xftG40BKKi8iH7XT+R2blzUvchIcBKU=

Did anyone ever try to line-up Coq in the programming language shoot-out?
http://shootout.alioth.debian.org/

Or any other dependently typed programming language?
Or any other proof assistant?

There is anecdotal evidence that Coq looses a factor between 5-50 in
speed to the extracted OCaml program.
It would be nice if we could substantiate this.

Best,

Bas

[Coq-Club] Programming language shootout for Coq?, Bas Spitters
- Re: [Coq-Club] Programming language shootout for Coq?, St�phane Glondu
  - Re: [Coq-Club] Programming language shootout for Coq?, Danko Ilik
  - Re: [Coq-Club] Programming language shootout for Coq?, Bas Spitters
    - Re: [Coq-Club] Programming language shootout for Coq?, Adam Koprowski
      - Re: [Coq-Club] Programming language shootout for Coq?, Greg Morrisett
        
        Re: [Coq-Club] Programming language shootout for Coq?, Adam Koprowski
- [Coq-Club] local definitions/proof environments, Vladimir Voevodsky
  - Re: [Coq-Club] local definitions/proof environments, Matthieu Sozeau
    - Re: [Coq-Club] local definitions/proof environments, AUGER
- Re: [Coq-Club] Programming language shootout for Coq?, Mathieu Boespflug