Lambda the Ultimate

We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits "fast and loose" reasoning without actually being loose...

Functional languages satisfy many pleasing equational laws, such as curry o uncurry = id, (fst x, snd x) = x and fst(x,y) = x and many others inspired by category theory. Such laws can be used to perform very pleasant proofs of program equality... There is just one problem. In real programming languages such as Haskell and ML, they do not hold.

However, not to worry: The authors show that if two closed terms have the same semantics for total functions, they have related semantics for partial functions.