Explicit renaming of bound variables

George Cherevichenko

We present some lambda calculus with explicit substitutions and named variables. The characteristic feature of this calculus is as follows: renaming of bound variables when perform…