Linearisation of the lambda-calculus and its termination

The notion of linearisation of the lambda-calculus has been explored in different settings: Damas and Florido used information given by intersection types, to define a notion of expansion of terms in the lambda-calculus into linear terms; Kfoury embedded the lambda-calculus into a new linear calculus, with a new notion of “linear” reduction, and linearization was defined indirectly by means of a notion of contraction of expanded terms in the new calculus into standard lambda-terms; Alves and Florido defined a notion of linearisation from standard lambda-terms into a linear subset, called the weak linear lambda-calculus, by using the notion of computation as paths, deriving from Lévy’s labelled lambda-calculus. In this talk we will explore these previous works, discuss their relation and present some open problems regarding the termination of linearisation methods.