  We study the semantics of an untyped lambda-calculus equipped with operators
representing read and write operations from and to a global state. We adopt the
monadic approach to model side effects and treat read and write as algebraic
operations over a computational monad. We introduce an operational semantics
and a type assignment system of intersection types, and prove that types are
invariant under reduction and expansion of term and state configurations, and
characterize convergent terms via their typings.
