Hi all!
I'm just started learning denotational semantics and have a simple question.
Suppose, we have simple language L (e.g. some form of lambda-calculus)
and have a semantic function: E : Term_L - Value.
Now, suppose, we extended our language with some additional side-effects
(e.g. state
I'm still getting my head around this myself, but I know a few
references that might help (maybe not directly, but they're in the
ballpark).
1 I believe the phrase natural lifting or naturality of liftings
is what you're after when you attempt to compare a monad and a bigger
monad that includes
[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
