Randy Pollack - Names, Binding and Substitution
If we take lambda-terms literally, problems of variable capture arise when defining substitution. Confusion between bound and free variables causes problems in other definitions as well, such as typing judgements. There are several well known approaches, e.g. nameless variables (de Bruijn indexes) and quotienting by alpha-conversion, but these have their own drawbacks. I will present an approach to binding and substitution using names that distinguishes between bound and free variables, and supports formal reasoning about terms as concrete objects (i.e. a datatype of terms). This approach has been used in a large formal development (by McKinna and Pollack) of some lambda calculus and type theory. I will compare this approach with some higher order representations recently proposed.