Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Programming language shootout for Coq?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Programming language shootout for Coq?


chronological Thread 
  • From: Adam Koprowski <adam.koprowski AT gmail.com>
  • To: Greg Morrisett <greg AT eecs.harvard.edu>
  • Cc: Bas Spitters <spitters AT cs.ru.nl>, St�phane Glondu <steph AT glondu.net>, Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Programming language shootout for Coq?
  • Date: Tue, 2 Mar 2010 13:23:41 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=RVZExLWN4QXN8uYbAMxBli6lMOjCDMMoq1EgiI/ixqONiVrDXiGAyVBNvGaBKdEtmQ 4ZdA4cxpmPDhcCNLwhfoBaGxQzDD7+vvsh62ZRGgz95KII9vH1S8PZ43BK6Rp7OG66mT OfRPB6u3V46UrjG7glEI0nuZhYgqc4GAZg6Xo=


2010/3/2 Greg Morrisett <greg AT eecs.harvard.edu>
Okay, but well, Haskell only provides IO by calling into C.
C only supports it by calling into assembly.  Assembly only
supports it by talking to the OS...  :-)
  ;-).  Sure, but my point was that if we want to use Ynot for IO then we can work/benchmark extracted code only. So if the interest is in benchmarking actual Coq's evaluation machinery then Ynot is not the answer... or am I wrong?

I actually think it's a fun thing for someone to do.
   Absolutely; agreed.
 
  Adam

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

Archive powered by MhonArc 2.6.16.

Top of Page