Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, finally.
Mon, Jul 27, 2009./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 Hutton — unwrap
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.