coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Bas Spitters <spitters AT cs.ru.nl>
Cc: 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:00:11 +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=wc1q2u7uTToYnibtt1Cy/q9pBC1/wU/Uw/XOZ6YnxcItKK0fVoHYQm2FZCpQmAFkwX WN69h760XAQwTFIcjl0N3T0IPjRMlUqEtD2fL1w266ROw51eOpfRvQpj2kqcmpjMEuEX FaS/mJUknzX+Ur7XFkdcCPARo9hPLxsYgdl4s=

��Dear Bas,

�

The Ynot library claims to support IO for Coq:
http://ynot.cs.harvard.edu/
but this may not be suitable for the shootout.

��They do, but again: that only works in extracted code (the IO primitives are stated as Coq axioms).

��Adam�

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

[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
  - Re: [Coq-Club] Programming language shootout for Coq?, Bas Spitters
    - Re: [Coq-Club] Programming language shootout for Coq?, Mathieu Boespflug
      - Re: [Coq-Club] Programming language shootout for Coq?, Bas Spitters
        
        Re: [Coq-Club] Programming language shootout for Coq?, Mathieu Boespflug