coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ryan Rusich <rusichr AT cs.ucr.edu>
- To: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- Cc: coq-club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] extraction of natural language from proofs
- Date: Sat, 6 Jun 2009 08:08:12 -0700
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=otVjF8OIv7HVDK5gww7GbpUildXUJyNUAwXTiDNpkSxnT6fAgWenuF7aG6JgC0e7iX KJhjOPZr1q5shhF4Rf/yXOnfpwutWJIBk+NL1WwIFFLe+ZZlI9TOrEyc7bcbXPh4Nh9E z7y19k3+X493mBjs7PCZz5xJDnqD4rNn4DEd0=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Deal All, Thank you for your time and assistance. This was indeed what I was inquiring about.
On Fri, Jun 5, 2009 at 11:50 PM, Yves Bertot <Yves.Bertot AT sophia.inria.fr> wrote:
If I remember correctly, the support for this command has been discontinued. The best documentation on this capability is documented in references 87, 95, 102 of http://www-sop.inria.fr/marelle/projet.html (today's version).Ryan Rusich wrote:
Dear All, Can anyone point me in the direction of the documentation for
extracting natural language from proofs using Coq? I read that it was
included in Coq from version 6.2 on, but have run into some difficulty
identifying the name of the command, and the location documentation
pertaining to it on the Coq website.
Thank you,
Ryan
We (the Lemme/Marelle team at INRIA Sophia) still have a tool chain that produces natural language text from proofs, but it is external to Coq, and we definitely have a hard time to maintain it. It is based on the Pcoq system, which is 50% compatible with the newest version of Coq (not all tactics are supported, the module system is not, notations are not, and so on).
The best references on this work are 47, 70, 71, 81, 87, 90, 92, 95, 100, 102, 104, 105.
I always dream of putting this software back on public distribution. It has some funny capabilities, but it is hard to maintain. We used it intensively for some of our first big proofs, but we don't anymore: we now use proof-general or coqide.
Yves
--
Cheers, Ryan
- [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs,
Guilhem Moulin
- Re: [Coq-Club] extraction of natural language from proofs, Lukasz Stafiniak
- Re: [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs, CHA Reeseo
- Re: [Coq-Club] extraction of natural language from proofs,
Yves Bertot
- Re: [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs,
Guilhem Moulin
Archive powered by MhonArc 2.6.16.