Linear explicit substitutions
Neil Ghani · Logic Journal of IGPL · 2000
The oe-calculus 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 oe-calculus to provide a linear calculus of explicit substitutions, called xDILL, which analogously describes the implementation of linear functional programming languages. Our main observation is that there are non-trivial interactions between linearity and explicit substitutions and that xDILL is therefore best understood as a synthesis of its underlying logical structure and the technology of explicit substitutions. This is in contrast to the oe-calculus where the explicit substitutions are independent of the underlying logical structure. Keywords: -calculus, explicit substitutions, linear logic 1 Introduction This paper combines the technologies of explicit substitutions and linearity in a mathematically consistent way. We start by describing these technologies and the...