Explicit substitutions

Authors:
  • MAM. Abadi
    M. Abadi
  • LCL. Cardelli
    L. Cardelli
  • PCP.-L. Curien
    P.-L. Curien
  • JLJ.-J. Levy
    J.-J. Levy

Abstract
The ��-calculus is a refinement of the �-calculus where substitu- tions are manipulated explicitly. The ��-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical �-calculus and concrete implementations.