S. Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, vol.111, issue.1-2, pp.3-57, 1993.
DOI : 10.1016/0304-3975(93)90181-R

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

F. Barbanera and S. Berardi, A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.
DOI : 10.1006/inco.1996.0025

H. P. Barendregt, The Lambda Calculus: its Syntax and Semantics. North- Holland, 1984.

H. P. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992.

H. P. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.37, issue.04, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

N. Benton, G. Bierman, V. De-paiva, and M. Hyland, A term calculus for Intuitionistic Linear Logic, 1st International Conference on Typed Lambda Calculus, TLCA '93, pp.75-90, 1993.
DOI : 10.1007/BFb0037099

R. Bloo and K. H. Rose, Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, Computer Science in the Netherlands, CSN '95, pp.62-72, 1995.

G. Boudol, The lambda-calculus with multiplicities, 4th International Conference on Concurrency Theory, CONCUR '93, pp.1-6, 1993.
DOI : 10.1007/3-540-57208-2_1

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

G. Boudol, P. Curien, and C. Lavatelli, A semantics for lambda calculi with resources, Mathematical Structures in Computer Science, vol.9, issue.4, pp.437-482, 1999.
DOI : 10.1017/S0960129599002893

G. Boudol and P. Zimmer, On Type Inference in the Intersection Type Discipline, Electronic Notes in Theoretical Computer Science, vol.136, pp.23-42, 2005.
DOI : 10.1016/j.entcs.2005.06.016

M. Coppo and M. Dezani-ciancaglini, A new type assignment for ??-terms, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.5, issue.1, pp.139-156, 1978.
DOI : 10.1007/BF02011875

URL : http://www.digizeitschriften.de/download/PPN379931524_0019/PPN379931524_0019___log16.pdf

M. Coppo and M. Dezani-ciancaglini, An extension of the basic functionality theory for the $\lambda$-calculus., Notre Dame Journal of Formal Logic, vol.21, issue.4, pp.685-693, 1980.
DOI : 10.1305/ndjfl/1093883253

P. Curien and H. Herbelin, The duality of computation, 5th International Conference on Functional Programming, ICFP'00, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

M. Dezani-ciancaglini and S. Ghilezan, Two Behavioural Lambda Models, Types for Proofs and Programs, pp.127-147, 2003.
DOI : 10.1007/3-540-39185-1_8

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

M. Dezani-ciancaglini, F. Honsell, and Y. Motohama, Compositional Characterizations of ??-Terms Using Intersection Types, 25th International Symposium on Mathematical Foundations of Computer Science, MFCS '00, pp.304-314, 2000.
DOI : 10.1007/3-540-44612-5_26

D. J. Dougherty, S. Ghilezan, and P. Lescanne, Characterizing strong normalization in the Curien???Herbelin symmetric lambda calculus: Extending the Coppo???Dezani heritage, Theoretical Computer Science, vol.398, issue.1-3, pp.114-128, 2008.
DOI : 10.1016/j.tcs.2008.01.022

T. Ehrhard and L. Regnier, The differential lambda-calculus, Theoretical Computer Science, vol.309, issue.1-3, pp.1-41, 2003.
DOI : 10.1016/S0304-3975(03)00392-X

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

J. and E. Santo, Completing Herbelin???s Programme, 9th International Conference on Typed Lambda Calculi and Applications, TLCA '07, pp.118-132
DOI : 10.1007/978-3-540-73228-0_10

J. E. Santo, S. Ghilezan, and J. Iveti´civeti´c, Characterising Strongly Normalising Intuitionistic Sequent Terms, International Workshop TYPES'07, pp.85-99, 2008.
DOI : 10.1007/978-3-540-68103-8_6

J. E. Santo, J. Iveti´civeti´c, and S. Likavec, Characterising strongly normalising intuitionistic terms, Fundamenta Informaticae, 2011.

J. Gallier, Typing untyped ?-terms, or reducibility strikes again! Annals of Pure and Applied Logic, pp.231-270, 1998.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935.
DOI : 10.1007/BF01201353

S. Ghilezan, Strong Normalization and Typability with Intersection Types, Notre Dame Journal of Formal Logic, vol.37, issue.1, pp.44-52, 1996.
DOI : 10.1305/ndjfl/1040067315

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

S. Ghilezan, J. Iveti´civeti´c, P. Lescanne, and D. Zuni´czuni´c, Intuitionistic Sequent-Style Calculus with Explicit Structural Rules, 8th International Tbilisi Symposium on Language, Logic and Computation, pp.101-124, 2011.
DOI : 10.1007/978-3-642-22303-7_7

URL : https://hal.archives-ouvertes.fr/ensl-00654762

S. Ghilezan and S. Likavec, Computational interpretations of logics, Papers, special issue Logic in Computer Science Mathematical Institute of Serbian Academy of Sciences and Arts, vol.20, issue.12, pp.159-215, 2009.

S. Ghilezan, J. Iveti´civeti´c, P. Lescanne, and S. Likavec, Intersection Types for the Resource Control Lambda Calculi, 8th International Colloquium on Theoretical Aspects of Computing, pp.116-134, 2011.
DOI : 10.1016/0304-3975(92)90297-S

URL : https://hal.archives-ouvertes.fr/ensl-00654755

S. Ghilezan and S. Likavec, Reducibility, ITRS '02, pp.106-123, 2002.
DOI : 10.1016/S1571-0661(04)80493-6

URL : http://doi.org/10.1016/s1571-0661(04)80493-6

J. Girard, Une extension de l'interprétation de Gödeì a l'analyse, et son applicationàplication`plicationà l'elimination des coupures dans l'analyse et la théorie des types, 2nd Scandinavian Logic Symposium, pp.63-92, 1971.

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

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

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, volume 7 of Cambridge Tracts in Theoret Computer Science, 1989.

H. Herbelin, A ??-calculus structure isomorphic to Gentzen-style sequent calculus structure, Computer Science Logic, CSL '94, pp.61-75, 1995.
DOI : 10.1007/BFb0022247

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

W. A. Howard, The formulas-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

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, 34th International Symposium on Mathematical Foundations of Computer Science, MFCS '09, pp.464-476, 2009.
DOI : 10.1007/BFb0014062

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

D. Kesner and F. Renaud, A prismoid framework for languages with resources, Theoretical Computer Science, vol.412, issue.37, pp.4867-4892, 2011.
DOI : 10.1016/j.tcs.2011.01.026

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

A. J. Kfoury and J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, vol.311, issue.1-3, pp.1-70, 2004.
DOI : 10.1016/j.tcs.2003.10.032

K. Kikuchi, Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi, 18th International Conference on Term Rewriting and Applications, RTA'07, pp.257-272, 2007.
DOI : 10.1007/978-3-540-73449-9_20

G. Koletsos, Church-Rosser theorem for typed functional systems, The Journal of Symbolic Logic, vol.32, issue.03, pp.782-790, 1985.
DOI : 10.2307/2274330

J. Krivine, Lambda-calcul types et modèles, 1990.

S. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-ciancaglini, and S. Van-bakel, Intersection types for explicit substitutions, Information and Computation, vol.189, issue.1, pp.17-42, 2004.
DOI : 10.1016/j.ic.2003.09.004

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

R. Matthes, Characterizing strongly normalizing terms of a calculus with generalized applications via intersection types, ICALP Satellite Workshops, pp.339-354, 2000.

J. C. Mitchell, Type Systems for Programming Languages, pp.415-431
DOI : 10.1016/B978-0-444-88074-1.50013-5

J. C. Mitchell, Foundation for Programmimg Languages, 1996.

P. M. Neergaard, THEORETICAL PEARLS: A bargain for intersection types: a simple strong normalization proof, Journal of Functional Programming, vol.15, issue.05, pp.669-677, 2005.
DOI : 10.1017/S0956796805005587

M. Pagani and S. Rocca, Solvability in Resource Lambda-Calculus, 13th International Conference on Foundations of Software Science and Computational Structures, pp.358-373, 2010.
DOI : 10.1007/978-3-642-12032-9_25

M. Parigot, ????-Calculus: An algorithmic interpretation of classical natural deduction, 3rd International Conference on Logic Programming and Automated Reasoning, LPAR '92, pp.190-201, 1992.
DOI : 10.1007/BFb0013061

L. Pinto and R. Dyckhoff, Sequent Calculi for the Normal Terms of the ????- and ???????-Calculi, Electronic Notes in Theoretical Computer Science, vol.17, pp.1-14, 1998.
DOI : 10.1016/S1571-0661(05)01182-5

G. Pottinger, A type assignment for the strongly normalizable ?-terms, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980.

]. 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

URL : http://doi.org/10.1016/0304-3975(94)90012-4

K. H. Rose, CRSX -Combinatory Reduction Systems with Extensions, 22nd International Conference on Rewriting Techniques and Applications of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.81-90, 2011.

K. H. Rose, Implementation Tricks That Make CRSX Tick. Talk at IFIP 1.6 workshop, 2011.

K. Rose, R. Bloo, and F. Lang, On Explicit Substitution with Names, Journal of Automated Reasoning, vol.19, issue.1, pp.1-26, 2011.
DOI : 10.1007/s10817-011-9222-5

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

P. Sallé, Une extension de la theorie des types en ??-calcul, 5th International Conference on Automata, Languages and Programming, ICALP '78, pp.398-410, 1978.
DOI : 10.1007/3-540-08860-1_30

P. Schroeder-heister and K. Do?en, Substructural Logics, 1993.

R. Statman, Logical relations and the typed ??-calculus, Information and Control, vol.65, issue.2-3, pp.85-97, 1985.
DOI : 10.1016/S0019-9958(85)80001-2

W. W. Tait, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, pp.198-212, 1967.
DOI : 10.1007/BF01447860

W. W. Tait, A realizability interpretation of the theory of species, Logic Colloquium, pp.240-251, 1975.
DOI : 10.1007/BFb0064875

S. Van-bakel, Complete restrictions of the intersection type discipline, Theoretical Computer Science, vol.102, issue.1, pp.135-163, 1992.
DOI : 10.1016/0304-3975(92)90297-S

V. Van-oostrom, Net-calculus. Course notes [62] D. ? Zuni´cZuni´c. Computing with sequents and diagrams in classical logic -calculi * X , d X and c X, 2001.