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
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
The Lambda Calculus: Its Syntax and Semantics, Revised edition, 1984. ,
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
The conservation theorem revisited, TLCA 1993, pp.163-178, 1993. ,
DOI : 10.1007/BFb0037105
Delayed Substitutions, RTA 2007, pp.169-183, 2007. ,
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
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
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
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
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
New notions of reduction and non-semantic proofs of beta-strong normalization in typed lambda-calculi, pp.311-321, 1995. ,
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
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
Réductions correctes et optimales dans le lambda-calcul, 1978. ,
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
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
Reasoning about programs in continuation-passing style, pp.288-298, 1992. ,
Monadic Translation of Intuitionistic Sequent Calculus, TYPES 2008, pp.100-116, 2009. ,