Calculi with explicit substitutions (ES) are widely used in different areas of computer science. Complex systems with ES were
developed these last 15 years to capture the good computational behaviour of the original systems (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 development
of such calculi. Then we use very simple technology to establish a general theory of explicit substitutions for the lambda-calculus
which enjoys fundamental properties such as simulation of one-step beta-reduction, confluence on metaterms, preservation of
beta-strong normalisation, strong normalisation of typed terms and full composition. The calculus also admits a natural translation
into Linear Logic’s proof-nets.