  This paper concerns the explicit treatment of substitutions in the lambda
calculus. One of its contributions is the simplification and rationalization of
the suspension calculus that embodies such a treatment. The earlier version of
this calculus provides a cumbersome encoding of substitution composition, an
operation that is important to the efficient realization of reduction. This
encoding is simplified here, resulting in a treatment that is easy to use
directly in applications. The rationalization consists of the elimination of a
practically inconsequential flexibility in the unravelling of substitutions
that has the inadvertent side effect of losing contextual information in terms;
the modified calculus now has a structure that naturally supports logical
analyses, such as ones related to the assignment of types, over lambda terms.
The overall calculus is shown to have pleasing theoretical properties such as a
strongly terminating sub-calculus for substitution and confluence even in the
presence of term meta variables that are accorded a grafting interpretation.
Another contribution of the paper is the identification of a broad set of
properties that are desirable for explicit substitution calculi to support and
a classification of a variety of proposed systems based on these. The
suspension calculus is used as a tool in this study. In particular, mappings
are described between it and the other calculi towards understanding the
characteristics of the latter.

Logic in Computer Science