20 Feb
2007
20 Feb
'07
11 a.m.
[my mail program hiccuped and chopped my message, sorry] 2 Another example that helped me when getting a feel for reasoning about monadic code (which is the basis of what we're doing here) was William Harrison's "Proof Abstraction for Imperative Languages". It uses monads and some of the notions like the ones you're in search of. 3 Lastly, we're reasoning about folds with denotational semantics. Graham Hutton's "Fold and Unfold for Program Semantics" was a great read for me. Using its techniques will likely shorten up any proof we've got. This is some of my favorite stuff, let me know how you fare with it! Good luck, Nick