Z. M. Ariola and H. Herbelin, Minimal Classical Logic and Control Operators, 30th International Colloquium on Automata, Languages and Programming, ICALP '03, pp.871-885, 2003.
DOI : 10.1007/3-540-45061-0_68

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.

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, 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

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

H. P. Barendregt and S. Ghilezan, Lambda terms for natural deduction, sequent calculus and cut elimination, Journal of Functional Programming, vol.10, issue.1, pp.121-134, 2000.
DOI : 10.1017/S0956796899003524

G. M. Bierman, A computational interpretation of the ?µ-calculus, 23rd International Symposium on Mathematical Foundations of Computer Science, MFCS '98, pp.336-345, 1998.

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

]. G. Bou93 and . Boudol, The lambda-calculus with multiplicities (abstract), 4th International Conference on Concurrency Theory, CONCUR '93, pp.1-6, 1993.

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.

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

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

M. Coppo, M. Dezani-ciancaglini, and B. Venneri, Principal type schemes and ?-calculus semantics, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.535-560, 1980.

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

]. A. Chu41 and . Church, The Calculi of Lambda-Conversion, 1941.

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, S. Ghilezan, and S. Likavec, Behavioural Inverse Limit Models, Theor. Comput Sci, vol.316, pp.1-349, 2004.
DOI : 10.1016/j.tcs.2004.01.023
URL : http://doi.org/10.1016/j.tcs.2004.01.023

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

. Ph and . De-groote, On the relation between the ?µ-calculus and the syntactic theory of sequential control, 5th International Conference on Logic Programming and Artificial Reasoning, LPAR'94, pp.31-43, 1994.

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

J. E. Santo, S. Ghilezan, and J. Iveti´civeti´c, Characterising strongly normalising intuitionistic sequent terms, International Workshop TYPES'07, pp.85-99, 2008.

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

J. , E. Santo, and L. Pinto, Permutative conversions in intuitionistic multiary sequent calculi with cuts, 6th International Conference on Typed Lambda Calculi and Applications, TLCA '03, pp.286-300, 2003.

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

J. and E. Santo, Delayed substitutions, 18th International Conference on Term Rewriting and Applications, RTA'07, pp.169-183, 2007.

J. Gallierghi96-]-s and . Ghilezan, Typing untyped ?-terms, or reducibility strikes again! Ann. Pure Appl. Logic Strong normalization and typability with intersection types, Notre Dame J. Formal Logic, vol.91, issue.371, pp.231-27044, 1996.

J. [. Ghilezan, P. Iveti´civeti´c, S. Lescanne, and . 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

J. [. Ghilezan, P. Iveti´civeti´c, D. Lescanne, and . 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

]. Gir71 and . Girard, Une extension de l'interprétation de Gödeì a l'analyse, et son applicationàapplication`applicationà 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

S. [. Ghilezan and . Likavec, Computational interpretations of logics, Mathematical Institute of Serbian Academy of Sciences and Arts, pp.159-215, 2009.

T. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

H. Herbelin, A lambda calculus structure isomorphic to Gentzen-style sequent calculus structure, Computer Science Logic, CSL '94, pp.61-75
URL : https://hal.archives-ouvertes.fr/inria-00381525

H. Herbelin and S. Ghilezan, An approach to call-by-name delimited continuations, 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pp.383-394, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00524949

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.

K. Kikuchi, Simple proofs of characterizing strong normalisation for explicit substitution calculi, 18th International Conference on Term Rewriting and Applications, RTA'07, pp.257-272, 2007.

D. Kesner and S. Lengrand, Resource operators for ??-calculus, Information and Computation, vol.205, issue.4, pp.419-473, 2007.
DOI : 10.1016/j.ic.2006.08.008
URL : https://hal.archives-ouvertes.fr/hal-00148539

]. S. Kle52 and . Kleene, Introduction to Metamathematics, 1952.

]. G. Kol85 and . Koletsos, Church-Rosser theorem for typed functionals, J. Symb. Logic, vol.50, pp.782-790, 1985.

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

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

R. Matthes, Characterizing strongly normalizing terms of a ?-calculus with generalized applications via intersection types, Carleton Scientific, 2000.

A. Mycroft, Using Kilim's Isolation Types for Multicore Efficiency, Invited talk at FoVeOOS 2011 -2nd International Conference on Formal Verification of Object-Oriented Software, 2011.

]. P. Nee05 and . Neergaard, Theoretical pearls: A bargain for intersection types: a simple strong normalization proof, J. Funct. Program, vol.15, issue.5, pp.669-677, 2005.

C. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.215-227, 1997.
DOI : 10.1145/263699.263722

M. Parigot, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, 3rd International Conference on Logic Programming and Automated Reasoning, LPAR '92, pp.190-201, 1992.

M. Parigot, Abstract, The Journal of Symbolic Logic, vol.50, issue.04, pp.1461-1479, 1997.
DOI : 10.1145/322358.322370

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.

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

]. L. Reg94 and . Regnier, Uné equivalence sur les lambda-termes, Theor. Comput Sci, vol.126, issue.2, pp.281-292, 1994.

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.

P. Sallé, Une extension de la théorie des types en lambda-calcul, 5th International Conference on Automata, Languages and Programming, ICALP '78, pp.398-410, 1978.

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

]. R. Sta85 and . Statman, Logical relations and the typed ?-calculus, Inform. Control, vol.65, pp.85-97, 1985.

M. H. Sørensen and P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 2006.

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, 2001.

. Zuni´czuni´c, Computing with sequents and diagrams in classical logic -calculi * X , d X and c X, 2007.