peteg's blog - hacking - isabelle - 2009 05 12 StreamFusion

Brian Huffman's soundness proofs for stream fusion

/hacking/isabelle | Link

I never post about anything technical I do any more, so instead I'll talk about someone else's stuff. Brian Huffman, HOLCF's last man standing, has a brand new entry in the Archive of Formal Proofs about verifying stream fusion. From a cursory read I thought he had opted for the "correct but GHC can't optimise it" variant floated in the original paper, but it turns out he has modelled the actual implementation. As always his proofs are mystifying in their clarity and succinctness.

Sweet, someone has ported the library to Standard ML.

Incidentally I stumbled upon VeriFun, which looks like it might be interesting, albeit inert. I wonder what their underlying logic is.