Intersection Types for a Computational Lambda-Calculus with Global State

We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce an operational semantics. The intersection type assignment system is indeed derived by solving a suitable domain equation in the category of omega-algebraic lattices; the solution consists of a filter-model generalizing the well-known construction for ordinary lambda-calculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the "type-semantics" property by construction. Finally, we prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.