Abstract Neil Ghani Valeria de Paiva Eike Ritter The -calculus 1 adds explicit substitutions to the -calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper generalises the -calculus to provide a linear calculus of explicit substitutions which analogously describes the implementation of linear functional programming languages.