This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not expressed within the calculus; the "freshness" conditions in such implicit calculi are a notorious source of errors.
[1] The concept has appeared in a large number of published papers in quite different fields, such as in abstract machines, predicate logic, and symbolic computation.
Therefore many calculi of explicit substitution avoid variable names altogether by using a so-called "name-free" De Bruijn index notation.
Explicit substitutions were sketched in the preface of Curry's book on Combinatory logic[2] and grew out of an ‘implementation trick’ used, for example, by AUTOMATH, and became a respectable syntactic theory in lambda calculus and rewriting theory.
Though it actually originated with de Bruijn,[3] the idea of a specific calculus where substitutions are part of the object language, and not of the informal meta-theory, is traditionally credited to Abadi, Cardelli, Curien, and Lévy.