Swapping: a natural bridge between named and indexed explicit   substitution calculi
  This article is devoted to the presentation of lambda_rex, an explicit substitution calculus with de Bruijn indexes and a simple notation. By being isomorphic to lambda_ex - a recent formalism with variable names -, lambda_rex accomplishes simulation of beta-reduction (Sim), preservation of beta-strong normalization (PSN) and meta-confluence (MC), among other desirable properties. Our calculus is based on a novel presentation of lambda_dB, using a swap notion that was originally devised by de Bruijn. Besides lambda_rex, two other indexed calculi isomorphic to lambda_x and lambda_xgc are presented, demonstrating the potential of our technique when applied to the design of indexed versions of known named calculi. 
Ariel Mendelzon (Departamento de Computaci\'on, FCEyN, Universidad de   Buenos Aires), Alejandro R\'ios (Departamento de Com...
cs.LO cs.PL