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 operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings.

We extend intersection types to a computational \(\lambda\) -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics but also in the type system . Since in the effectful setting, termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system can characterize the natural notion of observation, both in the finitary and in the infinitary setting. In a second phase, we extend our system with subtyping to incorporate a richer class of effects via monads on preorders instead of sets allowing us to model in particular non-determinism. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, for example, of typability and logical relation, to the monadic setting.

Abstract We extend intersection types to a computational $$\lambda $$ λ -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics, but also in the type system . Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.

We study the logical semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. Such a logic consists of an intersection type assignment system, which we derive from the denotational semantics of the calculus, based on the monadic approach to model computational λ-calculi. The system is obtained by constructing a filter model in the category of ω-algebraic lattices, such that the typing rules can be recovered out of the term interpretation. By construction, the so-obtained type system satisfies the “type-semantics” property and completeness.

Abstract We study the reduction in a $\lambda$ -calculus derived from Moggi’s computational one, which we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form and address the question of normalizing strategies. Our analysis relies on factorization results.

We study the semantics of an untyped λ-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 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.