Intersection Types and Computational Rules

The invariance of the meaning of a \u3bb-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements for a \u3bb-model. Being the intersection type systems a general framework for the study of semantic domains for the \u39b-calculus, the present paper provides a characterisation of "meaning invariance" in terms of characterisation results for intersection type systems enabling typing invariance of terms w.r.t. various notions of reduction/expansion, like \u3b2, \u3b7 and a number of relevant restrictions of their