M. Abadi, L. Cardelli, P. L. Curien, and J. Lévy, Explicit substitutions, Journal of Functional Programming, vol.4, issue.1, pp.375-416, 1991.
DOI : 10.1145/96709.96712
URL : https://hal.archives-ouvertes.fr/inria-00075382

B. Accattoli and S. Guerrini, Jumping Boxes, 2009.
DOI : 10.1142/9789812815149_0001

H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, of Studies in Logic and the Foundations of Mathematics, 1984.

R. Bloo, Preservation of Termination for Explicit Substitution, 1997.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-101, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

F. Kamareddine and A. Ríos, A ?-calculusàcalculusà la de Bruijn with explicit substitutions, PLILP, LNCS 982, 1995.

D. Kesner, The theory of explicit substitutions revisited, CSL, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00111285

D. Kesner, Perpetuality for Full and Safe Composition (in a Constructive Setting), ICALP, Part II, 2008.
DOI : 10.1007/978-3-540-70583-3_26
URL : https://hal.archives-ouvertes.fr/hal-00524782

D. Kesner and S. Lengrand, Resource operators for lambda-calculus. Information and Computation, pp.419-473, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00148539

D. Kesner and F. Renaud, The prismoid of resources Available as http

Z. Khasidashvili, Expression reduction systems, Proceedings of IN Vekua Institute of Applied Mathematics, 1990.
URL : https://hal.archives-ouvertes.fr/hal-00148530

J. Klop, Combinatory Reduction Systems, Mathematical Centre Tracts. Mathematisch Centrum, vol.127, 1980.

S. Lengrand, Normalisation and Equivalence in Proof Theory and Type Theory, 2006.

P. Lescanne and J. Rouyer-degli, The calculus of explicit substitutions ??, 1994.
URL : https://hal.archives-ouvertes.fr/inria-00074448

R. Milner, Local Bigraphs and Confluence: Two Conjectures, EXPRESS, ENTCS 175, 2006.
DOI : 10.1016/j.entcs.2006.07.035
URL : http://doi.org/10.1016/j.entcs.2006.07.035

T. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
DOI : 10.1109/LICS.1991.151658

F. Renaud, Preservation of strong normalisation for lambda-s Available on http, 2008.

V. Van-oostrom, Net-calculus. Course Notes available on http, 2001.