The theory of calculi with explicit substitutions revisited

Calculi with explicit substitutions are widely used in different areas of com-puter science such as functional and logic programming, proof-theory, theorem proving, concurrency, object-oriented languages, etc. Complex systems with ex-plicit substitutions were developed these last 15 years in order to capture the good computational behaviour of the original system (with meta-level substitutions) they were implementing. In this paper we first survey previous work in the domain by pointing out the motivations and challenges that guided the developement of such calculi. Then we use very simple technology to establish a general theory of explicit substitutions for the lambda-calculus which enjoys all the expected properties such as simulation of one-step beta-reduction, confluence on meta-terms, preservation of beta-strong normalisation, strong normalisation of typed terms and full composition. Also, the calculus we introduce turns out to admit a natural translation into Linear Logic’s proof-nets. 1 ha l-