Intersection Types for a Computational Lambda-Calculus with Global State

TL;DR

This paper develops a semantic framework for an untyped lambda-calculus with global state, using intersection types and monads to model side-effects, and characterizes convergent terms through typings.

Contribution

It introduces a novel intersection type system for lambda-calculus with global state, establishing invariance under reduction and characterizing convergence.

Findings

Types are invariant under reduction and expansion.

Convergent terms are characterized by their typings.

A monadic approach models read/write operations effectively.

Abstract

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.