coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] examples of program by extraction?

From: CHA Reeseo <reeseo AT formal.korea.ac.kr>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] examples of program by extraction?
Date: Wed, 20 May 2009 18:22:37 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type :content-transfer-encoding; b=e+0irHI5/wI/AspcIs3mlB0QinL/f8Fdgq0/BDfU7/+e0q7Uj84bRxUrWmx2UfNmz1 g+S86llYveBfN/+dBkMa24AHFThcU/6X+aNJMhi6bfKog51BD6yThMdeHIHLZfnWofZY GilvLR0NB7ZwiBxgKc3KlEVj6P63sQFVCHG+U=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

2009/5/20 Gyesik Lee
<gslee AT ropas.snu.ac.kr>:
> My point is to see some practical examples of "derivation of the
> program from its specification", e.g. in the software verification.
> Hopefully not so complicated ones.

Though I'm afraid I misunderstand what you meant by 'practical'
and I feel certain that you already know these,
how about Pierre Letouzey's paper "Extraction in Coq: An Overview"[1]
and several 'user contributions':

* http://www.lix.polytechnique.fr/coq/distrib/current/contribs/IPC.html
* http://www.lix.polytechnique.fr/coq/distrib/current/contribs/HigmanCF.html

If you meant something MORE practical,
such a example is what I'm also looking for nowadays. :^)

[1] http://www.springerlink.com/content/4k1j071432m57gp2/

--
CHA Reeseo
http://www.reeseo.net/

[Coq-Club] examples of program by extraction?, Gyesik Lee
- Re: [Coq-Club] examples of program by extraction?, CHA Reeseo
  - Re: [Coq-Club] examples of program by extraction?, Frederic Blanqui
- Message not available
  - Re: [Coq-Club] examples of program by extraction?, Gyesik Lee