Abstract: Implementing name bindings occurring in programming languages, types, and logical systems is not easy. In theory, the abstract thinking of the human mind can detect and avoid a possible variable capture. In implementation though, detecting variable capture requires clumsy auxiliary operations, which complicates formalization and proofs. Several name binding techniques have been proposed to have readable representations, capture-free substitutions, and intuitive proofs. However, their formalizations are quite different from theory: terms and proofs do not look like of theory. This paper proposes a name binding technique, substitutions and inference rules incorporating a term refreshing function comply with Barendregts variable convention, thus the formalization of formal systems almost identical to their theory. Untyped λ-calculus and simply typed λ-calculus are formalized to demonstrate the merits of this technique.

Key words: variable name, name binding, formal system, Barendregts variable convention, programming language theory