[Haskell-cafe] Equational Reasoning goes wrong

[Janis Voigtlaender]

I am surprised that no one has mentioned David Sands' work yet in this
thread. He has studied this issue extensively in the nineties (setting
out from an analogous problem as the one given in Neil's original post).
There are a number of papers that came out of this. The one probably
most immediately interesting for the problem at hand is:

"Total correctness by local improvement in the transformation of
functional programs"

http://portal.acm.org/citation.cfm?doid=227699.227716

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de