(Bologna University)

Linear logic decomposes intuitionistic implication in two connectives, the exponential modality and linear implication. Such a decomposition induces a new evaluation strategy, called linear head reduction, refining the key notion of head reduction in lambda-calculus. Linear head reduction (LHR) appeared very early in the linear logic literature. However, its presentations were intricate and hard to manipulate, so that it remained an exotic notion confined to the narrow circle of pure linear logicians. Recent progress in the theory of explicit substitutions provides a framework, the linear substitution calculus, where LHR admits a simple and manageable formulation. In this talk I will survey the new theory of LHR that arose recently, by revisiting and extending the results from the early days of linear logic. In particular, I will explain how LHR is the 'trait d'union' between explicit substitutions, proof-nets, the pi-calculus, Turing machines and Krivine abstract machine.Far-134 (video conferencing room)

Department of Computer Science