coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] examples of program by extraction?

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] examples of program by extraction?
Date: Wed, 20 May 2009 17:46:37 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type:content-transfer-encoding; b=ee8++A5Q9Po5sTiQgw/ZLAuXdqrAl0aQGuU1nMhTDaxLjgfT1ITbkmw5pXDB0H5JiV /pmUBlb19fDvdoe00cC2zilNpPb+wjyS0aKYw8d45o079c07eQpwJItJRQrL6PJ6iKdO xBz9zH1VqT57uyW0Nu/wNwPcyZ0tlCNO0h+gI=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq users,

I am looking for some practical examples of program by extraction using Coq.
I know I have to be careful with the word "practical", and I am not
sure if I understood well what is meant by "program by extraction".

Let me mention a phrase from Catarina Coquans's 1993 paper, "From
semantics to rules: A machine assisted analysis":

"It is well known that it is easier to prove the correctness of a
program if one derives the program from its specification rather than
first writing the program and then prove the correctness."

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.

To any indication i will be very grateful.

Thanks.

Gyesik

[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