Intersection types and Resource control in λ-calculus

The λ-calculus is a programming model based on functions. Its Turing-completeness comes from the freedom given to function constructions and function applications, but the λ-calculus thereby lacks some notions of control that are useful and natural both in programming and in mathematics. Typing systems provide such control, for instance by allowing the application of a fonction f, of “type ” A → B, to an argument e only if the latter is indeed of “type ” A. Basic typing systems will thus forbid a function to be applied to itself f(f), but they can be extended using intersection types: if f is of type (A → B)∩A (i.e. both of type A → B and of type A), then the above application makes sense. On the other hand, we introduced in [KL07] a version of λ-calculus with an explicit control of resources. An explicit component of this control is the duplication operator, which specifies the point in a program (and in its running) where some data (or more generally a term) needs to be duplicated. From this phenomenon come complexity issues, both in time and in space, and non-termination