Resource control and intersection types: an intrinsic connection

TL;DR

This paper explores the connection between resource control in lambda calculus and intersection types, introducing a new type system that characterizes strong normalization through variable roles and typeability.

Contribution

It presents a novel intersection type system for resource-controlled lambda calculus that links variable roles to intersection types and characterizes strong normalization.

Findings

Typeability of normal forms characterizes strong normalization.

A new decomposition of substitution into atomic steps.

Clear correspondence between variable roles and intersection types.

Abstract

In this paper we investigate the $\lambda$ -calculus, a $\lambda$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rules in the type assignment system. We introduce directly the class of $\lambda$ -terms and we provide a new treatment of substitution by its decompo-sition into atomic steps. We propose an intersection type assignment system for $\lambda$ -calculus which makes a clear correspondence between three roles of variables and three kinds of intersection types. Finally, we provide the characterisation of strong normalisation in $\lambda$ -calculus by means of an in-tersection type assignment system. This process uses typeability of normal forms, redex subject expansion and reducibility method.