The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Thank you very much for your answers although my question was a bit vague.
(I could not specify my question.)

What I learned from the answers is that many people are doing
intensive research on program extraction.
I will have look at the references and then try to start with something.

All the best,

Gyesik



On Sat, May 23, 2009 at 4:02 AM, Wouter Swierstra 
<wss AT cs.nott.ac.uk>
 wrote:
> Hi Gyesik,
>
>> I am looking for some practical examples of program by extraction using
>> Coq.
>
> I'm not sure if it counts as practical, but I recently had a paper accepted
> that really showcases some of the new "correct-by-construction" programming
> that is possible in Coq:
>
> http://www.cse.chalmers.se/~wouter/Publications/HoareStateMonad.pdf
>
> I've also implemented (most of) the core data types that are present in
> XMonad (a window manager written in Haskell) in Coq and proven some small
> properties. I'm working on getting the extracted Haskell code as close as
> possible to the original, hand-written version:
>
> http://www.haskell.org/pipermail/xmonad/2009-May/007881.html
>
> Hope these examples help. All the best,
>
>  Wouter
>