archives

GoF get SIGPLAN award

ACM SIGPLAN has given the 2005 Programming Languages Achievement Award to Erich Gamma, Richard Helm, Ralph Johnson and John Vlissides, authors of Design Patterns.

Fast and Loose Reasoning is Morally Correct

Nils Anders Danielsson, Jeremy Gibbons, John Hughes and Patrik Jansson (2005). Fast and Loose Reasoning is Morally Correct.

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.

Vacation

I am going on vacation, and will not be able to post or read LtU regularly until Aug. 25 .

I am sure the rest of the team will keep things in order until I get back. Play nice...