From Semantics to Types: the Case of the Imperative lambda-Calculus

TL;DR

This paper introduces an intersection type system for an imperative lambda-calculus with state, derived via domain equations and filter-models, ensuring soundness and completeness for reasoning about imperative programs.

Contribution

It presents a novel intersection type system for imperative lambda-calculus based on algebraic and domain-theoretic methods, extending existing models to handle stateful computations.

Findings

Type system is sound and complete.

Derived from domain equations in omega-algebraic lattices.

Generalizes known lambda-calculus models to imperative features.

Abstract

We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is 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, and it is sound and complete by construction.