B. Accattoli and D. Kesner, The Structural ??-Calculus, CSL 2010, pp.381-395, 2010.
DOI : 10.1007/978-3-642-15205-4_30

URL : https://hal.archives-ouvertes.fr/hal-00528228

B. Accattoli and D. Kesner, Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus, Logical Methods in Computer Science, vol.8, issue.1, 2011.
DOI : 10.2168/LMCS-8(1:28)2012

URL : https://hal.archives-ouvertes.fr/hal-00780319

H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Revised edition, 1984.

R. David, A short proof that adding some permutation rules to <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math> preserves <mml:math altimg="si2.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>S</mml:mi><mml:mi>N</mml:mi></mml:math>, Theoretical Computer Science, vol.412, issue.11, pp.1022-1026, 2011.
DOI : 10.1016/j.tcs.2010.10.048

P. De-groote, The conservation theorem revisited, TLCA 1993, pp.163-178, 1993.
DOI : 10.1007/BFb0037105

E. Santo and J. , Delayed Substitutions, RTA 2007, pp.169-183, 2007.

E. Santo and J. , A note on preservation of strong normalisation in the <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-calculus, Theoretical Computer Science, vol.412, issue.11, pp.1027-1032, 2011.
DOI : 10.1016/j.tcs.2010.10.049

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

J. R. Hindley, Reductions of residuals are finite, Transactions of the American Mathematical Society, vol.240, pp.345-361, 1978.
DOI : 10.1090/S0002-9947-1978-0489603-9

F. Kamareddine, Postponement, conservation and preservation of strong normalization for generalized reduction, Journal of Logic and Computation, vol.10, issue.5, pp.721-738, 2000.
DOI : 10.1093/logcom/10.5.721

D. Kesner, A Theory of Explicit Substitutions with Safe and Full Composition, Logical Methods in Computer Science, vol.5, issue.3, pp.1-29, 2009.
DOI : 10.2168/LMCS-5(3:1)2009

URL : https://hal.archives-ouvertes.fr/hal-00524735

A. J. Kfoury and J. B. Wells, New notions of reduction and non-semantic proofs of beta-strong normalization in typed lambda-calculi, pp.311-321, 1995.

J. Klop, V. Van-oostrom, and F. Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7

S. Lengrand, Termination of lambda-calculus with the extra call-by-value rule known as assoc. CoRR, abs/0806, p.4859, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00292029

J. Lévy, Réductions correctes et optimales dans le lambda-calcul, 1978.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
DOI : 10.1109/LICS.1989.39155

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787

L. Regnier, Une ??quivalence sur les lambda- termes, Theoretical Computer Science, vol.126, issue.2, pp.281-292, 1994.
DOI : 10.1016/0304-3975(94)90012-4

A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style, pp.288-298, 1992.

E. Santo, J. Matthes, R. Pinto, and L. , Monadic Translation of Intuitionistic Sequent Calculus, TYPES 2008, pp.100-116, 2009.