A typed lambda calculus with intersection types

The core of this paper is a new proposal for a true intersection typed lambda calculus, without any meta-level notion. Namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa. The main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables.