V. Abiteboul, S. Abiteboul, and V. Vianu, Fixpoint extensions of first-order logic and datalog-like languages, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.71-79, 1989.
DOI : 10.1109/LICS.1989.39160

. Alves, The Power of Linear Functions, Proceedings of the 20th International Workshop on Computer Science Logic (CSL '06), pp.119-134, 2006.
DOI : 10.1007/11874683_8

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

A. Asperti, Light affine logic, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pp.300-308, 1998.
DOI : 10.1109/LICS.1998.705666

R. Asperti, A. Asperti, and L. Roversi, Intuitionistic Light Affine Logic, ACM Transactions on Computational Logic, vol.3, issue.1, pp.137-175, 2002.
DOI : 10.1145/504077.504081

. Atassi, Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic, Proceedings of the 20th International Workshop on Computer Science Logic (CSL '06), pp.150-166, 2006.
DOI : 10.1007/11874683_10

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

P. Baillot, Checking Polynomial Time Complexity with Types, Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, pp.370-382, 2002.
DOI : 10.1007/978-0-387-35608-2_31

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

P. Baillot, Type inference for light affine logic via constraints on words, Theoretical Computer Science, vol.328, issue.3, pp.289-323, 2004.
DOI : 10.1016/j.tcs.2004.08.014

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

. Baillot, Light logics and optimal reduction: Completeness and complexity, Proceedings of the Twenty- Second Annual IEEE Symposium on Logic in Computer Science (LICS '07), pp.421-430, 2007.
DOI : 10.1109/lics.2007.27

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

V. Mogbil, Soft lambda-calculus: a language for polynomial time computation, Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures, pp.27-41, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00085129

. Baillot, . Terui, P. Baillot, and K. Terui, Light types for polynomial time computation in lambda-calculus, Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS '04), pp.266-275, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00003468

. Baillot, . Terui, P. Baillot, and K. Terui, A Feasible Algorithm for Typing in Elementary Affine Logic, Proceedings of the 8th International Conference on Typed Lambda-Calculi and Applications (TLCA '05), pp.55-70, 2005.
DOI : 10.1007/11417170_6

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

. Barendregt, . Ghilezan, H. 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

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

S. Bellantoni, Predicative recursion and computational complexity, 1992.

. Bellantoni, . Cook, S. Bellantoni, and S. Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.106, issue.2, pp.97-110, 1992.
DOI : 10.1515/9781400858927

. Bellantoni, Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.17-30, 2000.
DOI : 10.1016/S0168-0072(00)00006-3

URL : https://doi.org/10.1016/s0168-0072(00)00006-3

. Benton, A term calculus for Intuitionistic Linear Logic, Proceedings of the 1st International Conference on Typed Lambda-Calculi and Applications (TLCA '93), pp.75-90, 1993.
DOI : 10.1007/BFb0037099

G. Berry, Stable models of typed ??-calculi, Fifth International Colloquium on Automata, Languages and Programming -ICALP'78, pp.72-89, 1978.
DOI : 10.1007/3-540-08860-1_7

. Bierman, Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion, Electronic Notes in Theoretical Computer Science, vol.41, issue.3, p.41, 2000.
DOI : 10.1016/S1571-0661(04)80874-0

P. Clote, Computation models and function algebras, Proceedings of the International Workshop on Logic and Computational Complexity (LCC'94), pp.98-130, 1995.
DOI : 10.1007/3-540-60178-3_81

URL : http://www.cs.bc.edu/~clote/pub/handbook.ps

A. Cobham, The intrinsic computational difficulty of functions, Proceedings of the International Congress for Logic, Methodology, and Philosophy of Science, pp.24-30, 1964.

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

. Coppola, Elementary Affine Logic and the Call-by-Value Lambda Calculus, Proceedings of the 8th International Conference on Typed Lambda-Calculi and Applications (TLCA '05), volume 3461 of Lecture Notes in Computer Science, pp.131-145, 2005.
DOI : 10.1007/11417170_11

M. Coppola, P. Coppola, and S. Martini, Typing Lambda Terms in Elementary Logic with Linear Constraints, Proceedings of the 6th International Conference on Typed Lambda-Calculi and Applications (TLCA '01), pp.76-90, 2001.
DOI : 10.1007/3-540-45413-6_10

M. Coppola, P. Coppola, and S. Martini, Optimizing optimal reduction, ACM Transactions on Computational Logic, vol.7, issue.2, pp.219-260, 2006.
DOI : 10.1145/1131313.1131315

R. Coppola, P. Della-rocca-]-coppola, R. Della-rocca, and S. , Principal Typing in Elementary Affine Logic, Proceedings of the 7th International Conference on Typed Lambda-Calculi and Applications (TLCA '03), pp.90-104, 2003.
DOI : 10.1007/3-540-44904-3_7

P. Curien, Definability and Full Abstraction, Electronic Notes in Theoretical Computer Science, vol.172, pp.301-310, 2007.
DOI : 10.1016/j.entcs.2007.02.011

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

H. B. Curry, Modified basic functionality in combinatory logic, dialectica, vol.23, issue.2, 1969.
DOI : 10.1111/j.1746-8361.1969.tb01183.x

M. Damas, L. Damas, and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

V. Danos and J. Joinet, Linear logic and elementary time, Information and Computation, vol.183, issue.1, pp.123-137, 2003.
DOI : 10.1016/S0890-5401(03)00010-5

URL : https://doi.org/10.1016/s0890-5401(03)00010-5

. Danos, Abstract, The Journal of Symbolic Logic, vol.II, issue.03, pp.755-807, 1997.
DOI : 10.1007/BF00885763

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

D. De-carvalho-de-carvalho, Sémantiques de la logique linéaire et temps de calcul, 2007.

. Gaboardi, A logical account of PSPACE, 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL Proceedings. to appear, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00342323

. Gaboardi, . Paolini, M. Gaboardi, and L. Paolini, Syntactical, operational and denotational linearity, Workshop on Linear Logic, Ludics, Implicit Complexity and Operator Algebras, 2007.

R. Gaboardi, . Della-rocca, M. Gaboardi, R. Della-rocca, and S. , Soft linear logic and ?-calculus, 4th International Workshop on Proof, Computation, Complexity PCC'06, pp.Pro- ceedings, 2006.

R. Gaboardi, . Della-rocca, M. Gaboardi, R. Della-rocca, and S. , A Soft Type Assignment System for ??-Calculus, Proceedings of the 21st International Workshop on Computer Science Logic (CSL '07), pp.253-267, 2007.
DOI : 10.1007/978-3-540-74915-8_21

R. Giannini, P. Della-rocca-]-giannini, R. Della-rocca, and S. , A Type Inference Algorithm for a Stratified Polymorphic Type Discipline, Information and Computation, vol.109, issue.1-2, pp.115-173, 1994.
DOI : 10.1006/inco.1994.1015

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, Light Linear Logic, Information and Computation, vol.143, issue.2, pp.175-204, 1998.
DOI : 10.1006/inco.1998.2700

URL : https://doi.org/10.1006/inco.1998.2700

. Girard, Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, vol.97, issue.1, pp.1-66, 1992.
DOI : 10.1016/0304-3975(92)90386-T

A. Goerdt, Characterizing complexity classes by higher type primitive recursive definitions, Theoretical Computer Science, vol.100, issue.1, pp.45-66, 1992.
DOI : 10.1016/0304-3975(92)90363-K

C. A. Gunter, Semantics of Programming Languages: Structures and Techniques. foundations of Computing Series, 1992.

J. R. Hindley, The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, vol.146, pp.29-60, 1969.
DOI : 10.2307/1995158

M. Hofmann, Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.113-166, 2000.
DOI : 10.1016/S0168-0072(00)00010-5

URL : https://doi.org/10.1016/s0168-0072(00)00010-5

O. Hyland, J. M. Hyland, and C. L. Ong, On Full Abstraction for PCF: I, II, and III, Information and Computation, vol.163, issue.2, pp.285-408, 1994.
DOI : 10.1006/inco.2000.2917

N. Immerman, Descriptive Complexity, 1999.
DOI : 10.1007/978-1-4612-0539-5

N. Jones, The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, vol.11, issue.1, pp.55-94, 2001.
DOI : 10.1017/S0956796800003889

G. Kahn, Natural semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), pp.22-39, 1987.
DOI : 10.1007/BFb0039592

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

. Kfoury, . Wells, A. J. Kfoury, and J. B. Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order lambda-calculus, LISP and Functional Programming, pp.196-207, 1994.

J. Krivine, A call-by-name lambda calculus machine. Higher Order and Symbolic Computation, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00154508

Y. Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004.
DOI : 10.1016/j.tcs.2003.10.018

D. Leivant, A foundational delineation of computational feasibility, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.2-11, 1991.
DOI : 10.1109/LICS.1991.151625

M. Leivant, D. Leivant, and J. Marion, Lambda calculus characterizations of poly-time, Proceedings of the 1st International Conference on Typed Lambda-Calculi and Applications (TLCA '93), pp.274-288, 1993.
DOI : 10.1007/BFb0037112

M. Leivant, D. Leivant, and J. Marion, Ramified recurrence and computational complexity II: Substitution and poly-space, Proceedings of the 8th International Workshop on Computer Science Logic (CSL '94), volume 933 of Lecture Notes in Computer Science, pp.486-500, 1994.
DOI : 10.1007/BFb0022277

M. Leivant, D. Leivant, and J. Marion, Predicative functional recurrence and poly-space, Lecture Notes in Computer Science, vol.1214, pp.369-380, 1997.
DOI : 10.1007/BFb0030611

URL : https://link.springer.com/content/pdf/10.1007%2FBFb0030611.pdf

J. R. Longley, The sequentially realizable functionals. apal, pp.1-93, 2002.

H. G. Mairson and K. Terui, On the Computational Complexity of Cut-Elimination in Linear Logic, ICTCS, volume 2841 of Lecture Notes in Computer Science, pp.23-36, 2003.
DOI : 10.1007/978-3-540-45208-9_4

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

J. C. Mitchell, Type inference and type containment, Proc. of the international symposium on Semantics of data types, pp.257-277, 1984.
DOI : 10.1007/3-540-13346-1_13

J. C. Mitchell, Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988.
DOI : 10.1016/0890-5401(88)90009-0

URL : https://doi.org/10.1016/0890-5401(88)90009-0

P. Odifreddi, Classical Recursion Theory, 1999.

I. Oitavem, Implicit characterizations of pspace In Proof Theory in Computer Science, International Seminar, Proceedings, volume 2183 of Lecture Notes in Computer Science, pp.170-190, 2001.

C. L. Ong, Correspondence between operational and denotational semantics, Handbook of Logic in Computer Science, pp.269-356, 1995.

L. Paolini, A stable programming language, Information and Computation, vol.204, issue.3, pp.339-375, 2006.
DOI : 10.1016/j.ic.2005.11.002

G. D. Plotkin, LCF considerd as a programming language, Theoretical Computer Science, vol.5, pp.225-255, 1977.

G. D. Plotkin, A structural approach to operational semantics, First appeared as DAIMI FN?19 technical report Aarhus University, pp.60-6117, 1981.

D. Rémy, Simple, partial type-inference for system F based on type-containment, Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, pp.130-143, 2005.

[. , D. Rocca, R. Della-rocca, S. Roversi, and L. , Lambda calculus and intuitionistic linear logic, Studia Logica, issue.3, p.59, 1997.

W. J. Savitch, Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, vol.4, issue.2, pp.177-192, 1970.
DOI : 10.1016/S0022-0000(70)80006-X

URL : https://doi.org/10.1016/s0022-0000(70)80006-x

D. S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, vol.121, issue.1-2, pp.411-440, 1993.
DOI : 10.1016/0304-3975(93)90095-B

K. Terui, Linear logical characterization of polyspace functions (extended abstract), Presented at the Workshop on Implicit Computational Complexity ICC'00, p.2000, 2000.

K. Terui, Light affine lambda calculus and polytime strong normalization, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.209-220, 2001.
DOI : 10.1109/LICS.2001.932498

K. Terui, Light logic and polynomial time computation, 2002.

M. Vardi, Complexity and relational query languages, Fourteenth Symposium on Theory of Computing, pp.137-146, 1982.

J. B. Wells, Typability and type checking in the second-order ??-calculus are equivalent and undecidable, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.176-185, 1994.
DOI : 10.1109/LICS.1994.316068

J. B. Wells, Typability and type checking in System F are equivalent and undecidable, Annals of Pure and Applied Logic, vol.98, issue.1-3, pp.1-3111, 1999.
DOI : 10.1016/S0168-0072(98)00047-5