peteg's blog - hacking - isabelle - 2009 07 27 WorkerWrapper

Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, finally.

/hacking/isabelle | Link

Finally completed this bit of work, started sometime around December 2007. The Isabelle proofs available here remain a bit rough, but I did manage to find a bug in the original presentation by Andy Gill and Graham Huttonunwrap must be strict for fusion to be correct. From there it is a short step to a fusion rule that provably works. I've submitted a corrigendum-ish paper to the JFP and we'll see what happens now.