coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] extraction of natural language from proofs

From: Lukasz Stafiniak <lukstafi AT gmail.com>
To: Guilhem Moulin <guilhem.moulin AT ens-lyon.org>, Ryan Rusich <rusichr AT cs.ucr.edu>, coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] extraction of natural language from proofs
Date: Fri, 5 Jun 2009 18:19:51 +0200
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:content-transfer-encoding; b=DsKfHKz2tTWcbwpBODSbTAN6nVnCOXcRfCC2RNySUUnrBlmbyYjP53NI+m7/TlMe04 VtoqGj45q/cx92LIEMH5tTFadJBCK4qzQEK9N40P20gEon2b3OOUIheqe86rJCmTrABw pu4yVQvwIPM/DGPNeux9mEop66K2uAlZ0ehZw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Fri, Jun 5, 2009 at 5:24 PM, Guilhem Moulin
<guilhem.moulin AT ens-lyon.org>
wrote:
> I'm not sure that is what you looking for, but here is the relevant
> chapter of the reference manual:
> http://www.lix.polytechnique.fr/coq/distrib/v8.2/refman/Reference-Manual027.html
>

No, this is definitely not the thing being asked about. A quick search
led me to these interesting slides:
http://www-sop.inria.fr/lemme/Frederique.Guilhot/slides.pdf

[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