[TYPES] Explicit renaming of bound variables

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

 Hello.
I think I have  found "the right definition" of substitution and
alpha-conversion. Three main ideas are:
1) Contexts with multiplicity (i.e., repetitions of variables are
permitted);
2) A new form of explicit substitutions;
3) A new definition of free variables.
Renaming of bound variables when performing substitutions is done using
special reductions and may be delayed.
So far told two people: Lev Beklemishev and Mati Pentus (both like).
George.

http://arxiv.org/abs/1111.3171