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: Danko Ilik <dankoilik AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Programming language shootout for Coq?
  • Date: Tue, 2 Mar 2010 11:54:06 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=wAZSfUgOAabiEm6MHlNZX7uKJewQuiRyvImSyULutsprAh4TlukZZWcODtjXFNUWSi /AN32We+dxDkprtuLazP8zctRU9ZR/LmSm+WdykWgz1xfDFt2JrPMc0XjdUcnqKr2b9f f0XmtmMRMTDPFahBFFMZExgYj393GoN9OA35I=

On Tue, Mar 2, 2010 at 10:56 AM, Stéphane Glondu <steph AT glondu.net> wrote:
Another approach would be to wrap IOs in some kind of script, that would
parse the input, generate apropriate Coq input file, run it through
coqtop, then parse the output and turn it into the expected format. It
might be funny to compare Coq to other programming languages this way.
But this would also benchmark the pre/post-processing steps (for which
another language has to be chosen, too).

One could also run all the benchmarks inside one coqtop session, running "Time Eval vm_compute in (program input)", which would be a benchmark of Coq's virtual machine, without the pre-/post-processing overhead.

Danko



Archive powered by MhonArc 2.6.16.

Top of Page