Intersection types for explicit substitution with resource control

Abstract

We propose an intersection type assignment system for a term calculus with explicit substitution and resource control, which is due to the presence of weakening and contraction operators. The main contribution is the complete characterisation of strong normalisation of reductions using a combination of well-orders and suitable embeddings of terms as well as head subject expansion.