The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

CoLoR, a Coq Library on Rewriting and termination, is now using 
extraction to check the correctness of termination certificates. This is 
still under development but you can have a look at the Coq sources (see 
http://color.inria.fr). Best regards, Frederic.

CHA Reeseo a écrit :
> 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/