, A slice of a term is obtained by removing all components but one from each box. Let S(t) be the set of slices of term t defined as follows

, S(?) = {?} if ? ? {a

?. ,

, = {? 1

, S(! f (x ? ?a.a, ?a.a ? x)) = {! f (x ? ?a.a), ! f (?a.a ? x)}. As illustrated by this example, in general, a slice does not belong to the set of

, A term t is parsimonious if: 1. all its slices are affine, i.e. each variable occurs at most once in a slice, 2. box subterms do not contain free affine variables, 3. all exponential variables belong to a box subterm

?. ?a, a ? a is not parsimonious because of point 1. However, ?a.(?a.a)a is parsimonious

. ?-!-f, ? ?a.a, ?a.a ? x) is parsimonious. Indeed the affine variables a is not free and x occurs exactly once in each slice

, ? ! f (a, x, y, c) is not parsimonious because of point 2

, ? x?! f (y, z) is not parsimonious because of point 3. Characterizations of other interesting complexity classes based on the BSS model such as parallel polynomial time and classes of the polynomial hierarchy can be

. .. Bt09]), 11 1.2 Decidability and complexity of the type inference, Typing rules for LAL

. .. Decidability, 40 3.1 Big step operational semantics of imperative programs

. .. , Small step operational semantics of multi-threads

. .. , Small step operational semantics with deterministic scheduling, p.68

§. .. and |. .. , 90 3.15 Type system for the higher-order functional program, 69 3.7 Tier-based processes type system

, Non-uniform parsimonious logic type system

R. M. Amadio, N. Ayache, and F. Bobot, Certified Complexity (CerCo), FOPARA, pp.1-18, 2013.

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, COSTA: design and implementation of a cost and termination analyzer for Java bytecode, ESOP, pp.113-132, 2007.

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012.

N. Ayache, R. M. Amadio, and Y. Régis-gianas, Certifying and reasoning on cost annotations in C programs, FMICS, pp.32-46, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00702665

S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009.

V. Atassi, P. Baillot, and K. Terui, Verification of Ptime reducibility for system F terms: type inference in dual light affine logic, Logical Methods in Computer Science, vol.3, issue.4, 2007.

R. M. Amadio and S. Coupet-grimal, Silvano Dal Zilio, and Line Jakubiec. A functional scenario for bytecode verification of resource bounds, CSL, pp.265-279, 2004.

E. Albert, J. Correas, K. I. Einar-broch-johnsen, G. Pun, and . Román-díez, Parallel cost analysis. Transactions on Computational Logic, vol.19, issue.4, p.31, 2018.

M. Roberto, F. Amadio, and . Dabrowski, Feasible reactivity for synchronous cooperative threads, Electronic Notes in Theoretical Computer Science, vol.154, issue.3, pp.33-43, 2006.

B. Accattoli and U. Dal-lago, Beta reduction is invariant, indeed, CSL and LICS, pp.1-10, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091551

M. Avanzini and U. Dal-lago, Automating sized-type inference for complexity analysis, ICFP, vol.1, pp.1-29, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01639200

M. Avanzini and U. Dal-lago, On sharing, memoization, and polynomial time, Information and Computation, vol.261, pp.3-22, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01231816

M. Avanzini, U. D. Lago, and A. Ghyselen, Type-based complexity analysis of probabilistic functional programs, LICS, pp.1-13, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02381829

M. Avanzini, U. D. Lago, and G. Moser, Analysing the complexity of functional programs: higher-order meets first-order, ICFP, vol.50, pp.152-164, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01231809

M. Avanzini, U. D. Lago, and A. Yamada, On probabilistic term rewriting, FLOPS, pp.132-148, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02381877

M. Roberto, S. Amadio, and . Dal-zilio, Resource control for synchronous cooperative threads, CONCUR, pp.68-82, 2004.

M. Avanzini, N. Eguchi, and G. Moser, A new order-theoretic characterisation of the polytime computable functions, Theoretical Computer Science, vol.585, pp.3-24, 2015.

E. Albert, J. Correas-fernández, and G. Román-díez, Noncumulative resource analysis, TACAS, pp.85-100, 2015.

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.

E. Albert, S. Genaim, and M. Gomez-zamalloa, Heap space analysis for Java bytecode, ISMM, pp.105-116, 2007.

E. Albert, S. Genaim, and M. Gómez-zamalloa, Heap space analysis for garbage collected languages, Science of Computer Programming, vol.78, issue.9, pp.1427-1448, 2013.

J. Avery, L. Kristiansen, and J. Moyen, Static complexity analysis of higher order programs, FOPARA, pp.84-99, 2009.

B. Allen, Arithmetizing uniform NC, Annals of Pure and Applied Logic, vol.53, issue.1, pp.1-50, 1991.

M. Avanzini and G. Moser, Complexity analysis by rewriting, FLOPS, pp.130-146, 2008.

M. Avanzini and G. Moser, Dependency pairs and polynomial path orders, RTA, pp.48-62, 2009.

M. Avanzini and G. Moser, Closing the gap between runtime complexity and polytime computability, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, pp.33-48, 2010.

M. Avanzini and G. Moser, Complexity analysis by graph rewriting, FLOPS, pp.257-271, 2010.

R. Atkey and C. Mcbride, Productive coprogramming with guarded recursion, ICFP, vol.48, pp.197-208, 2013.

M. Avanzini and G. Moser, Tyrolean complexity tool: Features and usage, RTA, volume 21 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2013.

M. Avanzini and G. Moser, A combination framework for complexity. Information and Computation, vol.248, pp.22-55, 2016.

R. M. Amadio, Max-plus quasi-interpretations, TLCA, pp.31-45
URL : https://hal.archives-ouvertes.fr/hal-00146999

. Springer, , 2003.

R. M. Amadio, Synthesis of max-plus quasi-interpretations, Fundamenta Informaticae, vol.65, issue.1-2, pp.29-60, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00146968

M. Avanzini, G. Moser, and M. Schaper, TcT: Tyrolean complexity Tool, TACAS, pp.407-423, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01392188

M. Avanzini, G. Moser, and M. Schaper, Modular runtime complexity analysis of probabilistic while programs. DICE-FOPARA workshops, 2019.

A. Asperti and L. Roversi, Intuitionistic light affine logic, Transactions on Computational Logic, vol.3, issue.1, pp.137-175, 2002.

A. Asperti, Light affine logic, LICS, pp.300-308, 1998.

M. Avanzini, POP* and semantic labeling using SAT, ESSLLI, pp.155-166, 2008.

H. P. Barendregt, The Lambda Calculus, vol.3, 1984.

A. Ben-amram, General size-change termination and lexicographic descent, The essence of computation, pp.3-17, 2002.

A. Ben, -. , and S. Genaim, On the linear ranking problem for integer linear-constraint loops, POPL, vol.48, pp.51-62, 2013.

A. Ben, -. , and S. Genaim, On multiphase-linear ranking functions, CAV, pp.601-620, 2017.

A. Ben-amram, S. Genaim, and A. Masud, On the termination of integer loops, Transactions on Programming Languages and Systems, vol.34, issue.4, p.16, 2012.

P. Baillot, Checking polynomial time complexity with types, Foundations of Information Technology in the Era of Network and Mobile Computing, pp.370-382, 2002.
URL : https://hal.archives-ouvertes.fr/hal-00084626

P. Baillot, Stratified coherence spaces: a denotational semantics for light linear logic, Theoretical Computer Science, vol.318, issue.1-2, pp.29-55, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00084609

P. Baillot, Type inference for light affine logic via constraints on words, Theoretical Computer Science, vol.328, issue.3, pp.289-323, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00084611

P. Baillot, Logique linéaire, types et complexité implicite. Mémoire d'habilitation à diriger des recherches, 2008.

P. Baillot, E. D. Benedetti, and S. Rocca, Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, vol.261, pp.55-77, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01015171

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

O. Bournez, F. Cucker, P. Jacobé-de-naurois, and J. Marion, Implicit complexity over an arbitrary structure: Sequential and parallel polynomial time, Journal of Logic and Computation, vol.15, issue.1, pp.41-58, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00102942

O. Bournez, F. Cucker, P. Jacobé-de-naurois, and J. Marion, Implicit complexity over an arbitrary structure: Quantifier alternations. Information and Computation, vol.204, pp.210-230, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00107811

G. Bonfante, A. Cichon, J. Marion, and H. Touzet, Complexity classes and rewrite systems with polynomial interpretation, CSL, pp.372-384, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098689

G. Bonfante, A. Cichon, J. Marion, and H. Touzet, Algorithms with polynomial interpretation termination proof, Journal of Functional Programming, vol.11, issue.1, pp.33-53, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100819

M. J. Burrell, J. B. Robin, B. F. Cockett, and . Redmond, Pola: A language for ptime programming, FICS, pp.7-8, 2009.

G. Bonfante and F. Deloup, Complexity invariance of real interpretations, TAMC, pp.139-150, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00535784

G. Bonfante, F. Deloup, and A. Henrot, Real or natural number interpretation and their effect on complexity, Theoretical Computer Science, vol.585, pp.25-40, 2015.

P. Baillot and U. Dal-lago, Higher-order interpretations and program complexity, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.16, pp.62-76, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00798298

P. Baillot and U. Dal-lago, Higher-order interpretations and program complexity, Information and Computation, vol.248, pp.56-81, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00798298

F. Breuvart and U. Dal-lago, On intersection types and probabilistic lambda calculi, PPDP, vol.8, pp.1-13, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926420

J. Borgström, U. D. Lago, A. D. Gordon, and M. Szymczak, A lambda-calculus foundation for universal probabilistic programming, ICFP, vol.51, pp.33-46, 2016.

P. Baillot, U. D. Lago, and J. Moyen, On quasi-interpretations, blind abstractions and implicit complexity, Mathematical Structures in Computer Science, vol.22, issue.4, pp.549-580, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00798377

S. Bellantoni, Predicative recursion and the polytime hierarchy, Feasible Mathematics II, pp.15-29, 1995.

O. Bournez and F. Garnier, Proving positive almost-sure termination, RTA, pp.323-337, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00099867

O. Bournez and F. Garnier, Proving positive almost sure termination under strategies, RTA, pp.357-371, 2006.

G. Bonfante and Y. Guiraud, Programs as polygraphs: computability and complexity, 2007.

G. Bonfante and Y. Guiraud, Intensional properties of polygraphs, Electronic Notes in Theoretical Computer Science, vol.203, issue.1, pp.65-77, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00129391

P. Baillot and A. Ghyselen, Combining linear logic and size types for implicit complexity, CSL, volume 119 of LIPIcs, pp.1-21, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01948196

O. Bournez, W. Gomaa, and E. Hainry, Algebraic characterizations of complexity-theoretic classes of real functions, International Journal of Unconventional Computing, vol.7, issue.5, pp.331-351, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00421561

O. Bournez, D. S. Graça, and A. Pouly, Polynomial time corresponds to solutions of polynomial ordinary differential equations of polynomial length: The general purpose analog computer and computable analysis are two efficiently equivalent models of computations, ICALP, vol.55, pp.1-15, 2016.

G. Barthe, B. Grégoire, and C. Riba, Type-based termination with sized products, CSL, pp.493-507, 2008.

O. Bournez and E. Hainry, Real recursive functions and real extensions of recursive functions, MCU, pp.116-127, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00100053

L. Beringer, M. Hofmann, A. Momigliano, and O. Shkaravska, Automatic certification of heap consumption, LPAR, pp.347-362, 2004.

K. J. Biba, Integrity considerations for secure computer systems, 1977.

G. Bonfante, R. Kahle, J. Marion, and I. Oitavem, Recursion schemata for NC k, CSL, pp.49-63, 2008.

A. Bucciarelli, D. Kesner, and D. Ventura, Non-idempotent intersection types for the lambda-calculus, Logic Journal of the IGPL, vol.25, issue.4, pp.431-464, 2017.

A. Bernadet and S. Lengrand, Complexity of strongly normalising ?terms via non-idempotent intersection types, FoSSaCS, pp.88-107, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01110489

S. Bloch, Function-algebraic characterizations of log and polylog parallel time, Computational Complexity, vol.4, issue.2, pp.175-205, 1994.

C. Borralleras, S. Lucas, A. Oliveras, E. Rodríguez-carbonell, and A. Rubio, Sat modulo linear arithmetic for solving polynomial constraints, Journal of Automated Reasoning, vol.48, issue.1, pp.107-131, 2012.

D. E. Bell and L. J. Padula, Secure computer system: unified exposition and multics interpretation, Mitre corp Rep, 1976.

M. Blum, A machine-independent theory of the complexity of recursive functions, Journal of the ACM, vol.14, issue.2, pp.322-336, 1967.

P. Baillot and V. Mogbil, Soft lambda-calculus: a language for polynomial time computation, FoSSaCS, pp.27-41, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00085129

P. Baillot and D. Mazza, Linear logic by levels and bounded time complexity, Theoretical Computer Science, vol.411, issue.2, pp.470-503, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00488531

A. Brunel and A. Madet, Indexed realizability for bounded-time programming with references and type fixpoints, APLAS, pp.264-279, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00735584

G. Bonfante, J. Marion, and J. Moyen, On lexicographic termination ordering with space bound certifications, PSI, pp.482-493
URL : https://hal.archives-ouvertes.fr/inria-00100523

. Springer, , 2001.

G. Bonfante, J. Marion, and J. Moyen, Quasiinterpretations and small space bounds, RTA, pp.150-164, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00001234

G. Bonfante, J. Marion, and J. Moyen, Quasiinterpretations a way to control resources, Theoretical Computer Science, vol.412, issue.25, pp.2776-2796, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591862

G. Bonfante, J. Marion, J. Moyen, and R. Péchoux, Synthesis of quasi-interpretations, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000660

G. Bonfante, J. Marion, and R. Péchoux, A characterization of alternating log time by first order functional programs, LPAR, pp.90-104
URL : https://hal.archives-ouvertes.fr/inria-00110014

. Springer, , 2006.

G. Bonfante, J. Marion, and R. Péchoux, Quasiinterpretation synthesis by decomposition, ICTAC, pp.410-424, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00130920

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

S. Bellantoni, K. Niggl, and H. Schwichtenberg, Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.17-30, 2000.

. Peter-van-emde and . Boas, Machine models and simulations, Handbook of Theoretical Computer Science, vol.1, pp.1-66, 2014.

G. Bonfante, Some programming languages for Logspace and Ptime, AMAST, pp.66-80, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00105744

G. Bonfante, Complexité implicite des calculs : interprétation de programmes. Mémoire d'habilitation à diriger des recherches, 2011.

A. Barber and G. Plotkin, Dual intuitionistic linear logic, 1996.

P. Baillot and M. Pedicini, An embedding of the BSS model of computation in light affine lambda-calculus, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00085547

E. D. Benedetti and S. Rocca, Call-by-value, elementary time and intersection types, FOPARA, pp.40-59, 2015.

L. Blum, M. Shub, and S. Smale, On a theory of computation over the real numbers; NP completeness, recursive functions and universal machines, FOCS, pp.387-397, 1988.

P. Baillot and K. Terui, Light types for polynomial time computation in lambda-calculus, LICS, pp.266-275, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00003468

P. Baillot and K. Terui, A feasible algorithm for typing in elementary affine logic, TLCA, pp.55-70, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00084629

P. Baillot and K. Terui, Light types for polynomial time computation in lambda calculus, Information and Computation, vol.207, issue.1, pp.41-62, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00003468

A. Brunel and K. Terui, Church => Scott = Ptime: an application of resource sensitive realizability, Electronic Proceedings in Theoretical Computer Science, vol.23, pp.31-46, 2010.

E. Bernstein and U. Vazirani, Quantum complexity theory, SIAM Journal on Computing, vol.26, issue.5, pp.1411-1473, 1997.

R. Clouston and A. Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. Programming and reasoning with guarded recursion for coinductive types, FoS-SaCS, pp.407-421, 2015.

P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL, pp.238-252, 1977.

W. Chin and J. Darlington, A higher-order removal method, Lisp and Symbolic Computation, vol.9, pp.287-322, 1996.

Q. Carbonneaux, J. Hoffmann, and Z. Shao, Compositional certified resource bounds, vol.50, pp.467-478, 2015.

A. Stephen, B. M. Cook, and . Kapron, Characterizations of the basic feasible functionals of finite type, Feasible mathematics, pp.71-96, 1990.

P. Clote and J. Krajícek, Arithmetic, Proof Theory, and Computational Complexity. Number 23, 1993.

W. Chin and S. Khoo, Calculating sized types. Higher-Order and Symbolic Computation, vol.14, pp.261-300, 2001.

A. Ben-cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, vol.9, pp.137-159, 1987.

A. Cichon and P. Lescanne, Polynomial interpretations and the complexity of algorithms, CADE, pp.139-147, 1992.

P. Clote, Sequential, machine-independent characterizations of the parallel complexity classes Alogtime, AC k , NC k and NC, Feasible mathematics, pp.49-69, 1990.

P. Clote, Nondeterministic stack register machines, Theoretical Computer Science, vol.178, issue.1-2, pp.37-76, 1997.

P. Clote, Computation models and function algebras, Studies in Logic and the Foundations of Mathematics, vol.140, pp.589-681, 1999.

A. Cichon and J. Marion, The light lexicographic path ordering, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099238

P. Coppola and S. Martini, Typing lambda terms in elementary logic with linear constraints, TLCA, pp.76-90, 2001.

E. Contejean, C. Marché, A. P. Tomás, and X. Urbain, Mechanically proving termination using polynomial interpretations, Journal of Automated Reasoning, vol.34, issue.4, p.325, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00001167

L. Manuel, K. Campagnolo, and . Ojakian, Using approximation to relate computational classes over the reals, MCU, pp.39-61, 2007.

A. Cobham, The intrinsic computational difficulty of functions, 1965.

L. Colson, About primitive recursive algorithms, ICALP, pp.194-206

. Springer, , 1989.

R. L. Constable, Type two computational complexity, STOC, pp.108-121, 1973.

A. Stephen and . Cook, Computability and complexity of higher type functions, Logic from Computer Science, pp.51-72, 1992.

T. Coquand, Infinite objects in type theory, TYPES, vol.806, pp.62-78, 1994.

B. Cook, A. Podelski, and A. Rybalchenko, TERMINATOR: beyond safety, CAV, pp.415-418, 2006.

A. Stephen, C. Cook, and . Rackoff, Space lower bounds for maze threadability on restricted machines, SIAM Journal on Computing, vol.9, issue.3, pp.636-652, 1980.

A. Chandra and L. Stockmeyer, Alternation, FOCS, pp.98-108, 1976.

J. Chrzaszcz and A. Schubert, ML with Ptime complexity guarantees, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.16, pp.198-212, 2012.

J. Chrzaszcz and A. Schubert, The role of polymorphism in the characterisation of complexity by soft types. Information and Computation, vol.248, pp.130-149, 2016.

P. Clote and G. Takeuti, First order bounded arithmetic and small boolean circuit complexity classes, Feasible mathematics, pp.154-218, 1995.

A. Stephen, A. Cook, and . Urquhart, Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic, vol.63, issue.2, pp.103-200, 1993.

O. Danvy, An analytical approach to program as data objects, 2006.

C. Daniel-de, Intersection types for light affine lambda calculus, Electronic Notes in Theoretical Computer Science, vol.136, pp.133-152, 2005.

C. Daniel-de, Execution time of ?-terms via denotational semantics and intersection types, Mathematical Structures in Computer Science, vol.28, issue.7, pp.1169-1203, 2018.

N. Dershowitz, A note on simplification orderings, Information Processing Letters, vol.9, issue.5, pp.212-215, 1979.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.

N. Dershowitz, Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1/2, pp.69-116, 1987.

D. Deutsch, Quantum theory, the Church-Turing principle and the universal quantum computer, Mathematical and Physical Sciences, vol.400, pp.97-117, 1818.

W. Edsger and . Dijkstra, On the productivity of recursive definitions, vol.749, 1980.

V. Danos and J. Joinet, Linear logic and elementary time, formation and Computation, vol.183, pp.123-137, 2003.

U. Dal-lago and M. Gaboardi, Linear dependent types and relative completeness, LICS, pp.133-142, 2011.

U. Dal-lago and C. Grellois, Probabilistic termination by monadic affine sized typing, Transactions on Programming Languages and Systems, vol.41, issue.2, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01635077

U. Dal-lago and M. Hofmann, Quantitative models and implicit complexity, FSTTCS, pp.189-200, 2005.

U. Dal-lago and M. Hofmann, Realizability models and implicit complexity, Theoretical Computer Science, vol.412, issue.20, pp.2029-2047, 2011.

U. Dal-lago and S. Martini, On constructor rewrite systems and the lambda-calculus, ICALP, pp.163-174, 2009.

U. Dal-lago, S. Martini, and D. Sangiorgi, Light logics and higherorder processes, Electronic Proceedings in Theoretical Computer Science, vol.41, pp.46-60, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01400903

U. Dal-lago, S. Martini, and D. Sangiorgi, Light logics and higherorder processes, Mathematical Structures in Computer Science, vol.26, issue.6, pp.969-992, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01400903

U. Dal-lago, A. Masini, and M. Zorzi, Quantum implicit computational complexity, Theoretical Computer Science, vol.411, issue.2, pp.377-409, 2010.

U. Dal-lago and B. Petit, Linear dependent types in a call-by-value scenario, Science of Computer Programming, vol.84, pp.77-100, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00909317

N. Danner, D. R. Licata, and R. Ramyaa, Denotational cost semantics for functional languages with inductive types, ICFP, vol.50, pp.140-151, 2015.

U. Dal-lago and U. Schöpp, Functional programming in sublinear space, ESOP, pp.205-225, 2010.

U. Dal-lago and U. Schöpp, Computation by interaction for space-bounded functional programming. Information and Computation, vol.248, pp.150-194, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01337724

U. Dal-lago and P. Parisen-toldin, Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop. Productivity of stream definitions, Theoretical Computer Science, vol.241, issue.4-5, pp.765-782, 2010.

T. Ehrhard and L. Regnier, The differential lambda-calculus, Theoretical Computer Science, vol.309, issue.1-3, pp.1-41, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00150572

T. Ehrhard and L. Regnier, Uniformity and the taylor expansion of ordinary lambda-terms, Theoretical Computer Science, vol.403, issue.2-3, pp.347-372, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00150275

J. Endrullis, J. Waldmann, and H. Zantema, Matrix interpretations for proving termination of term rewriting, Journal of Automated Reasoning, vol.40, issue.2-3, pp.195-220, 2008.

R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets, Complexity of computation, vol.7, pp.43-73, 1974.

C. Faggian, Probabilistic rewriting: Normalization, termination, and unique normal forms, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.1-25, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02411553

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-kamp, R. Thiemann et al., SAT solving for termination analysis with polynomial interpretations, SAT, pp.340-354, 2007.

H. Férée, E. Hainry, M. Hoyrup, and R. Péchoux, Interpretation of stream programs: Characterizing type 2 polynomial time complexity, ISAAC, pp.291-303, 2010.

H. Férée, E. Hainry, M. Hoyrup, and R. Péchoux, Characterizing polynomial time complexity of stream programs using interpretations, Theoretical Computer Science, vol.585, pp.41-54, 2015.

H. Férée, S. Hym, M. Mayero, J. Moyen, and D. Nowak, Formal proof of polynomial-time complexity with quasi-interpretations, CPP, pp.146-157, 2018.

C. Faggian, S. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes et al., Analyzing program termination and complexity automatically with AProVE, LICS, vol.58, pp.3-31, 2017.

O. Geupel, Terminationsbeweise bei Termersetzungssystemen. diplomarbeit, 1988.

J. Giesl, Generating polynomial orderings for termination proofs, RTA, pp.426-431, 1995.

J. Girard, Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-101, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Light linear logic. Information and Computation, vol.143, pp.175-204, 1998.

S. Gimenez and G. Moser, The complexity of interaction, POPL, vol.51, pp.243-255, 2016.

S. Gulwani, K. Krishna, T. Mehra, and . Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, POPL, vol.44, pp.127-139, 2009.

M. Gaboardi, J. Marion, and S. Rocca, A logical account of PSPACE, vol.43, pp.121-131, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00342323

M. Gaboardi, J. Marion, and S. Rocca, Soft linear logic and polynomial complexity classes, Electronic Notes in Theoretical Computer Science, vol.205, pp.67-87, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00342320

I. Gnaedig, Induction for positive almost sure termination, PPDP, pp.167-178, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00182435

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für mathematik und physik, vol.38, pp.173-198, 1931.

A. Goerdt, Characterizing complexity classes by general recursive definitions in higher types, Information and Computation, vol.101, issue.2, pp.202-218, 1992.

M. Gaboardi and R. Péchoux, Global and local space properties of stream programs, FOPARA, pp.51-66, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00539835

M. Gaboardi and R. Péchoux, Upper bounds on stream I/O using semantic interpretations, CSL, pp.271-286, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00431469

M. Gaboardi and R. Péchoux, Algebras and coalgebras in the light affine lambda calculus, ICFP, vol.50, pp.114-126, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01112165

M. Gaboardi and R. Péchoux, On bounding space usage of streams using interpretation analysis, Science of Computer Programming, vol.111, pp.395-425, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01112161

E. Grädel, The expressive power of second order Horn logic, STACSs, pp.466-477, 1991.

B. Gramlich, Generalized sufficient conditions for modular termination of rewriting, Communication and Computing, vol.5, issue.3-4, pp.131-158, 1994.

M. Gaboardi and S. Rocca, A soft type assignment system for ?-calculus, CSL, pp.253-267, 2007.

M. Gaboardi and S. Rocca, Type inference for a polynomial lambda calculus, TYPES, pp.136-152, 2008.

K. Lov and . Grover, A fast quantum mechanical algorithm for database search, STOC, pp.212-219, 1996.

A. Grzegorczyk, Some classes of recursive functions, stytut Matematyczny Polskiej Akademi Nauk (Warszawa), 1953.

J. Girard, A. Scedrov, and P. Scott, Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, vol.97, issue.1, pp.1-66, 1992.

S. Gulwani, SPEED: Symbolic complexity bound analysis, CAV, pp.51-62, 2009.

Y. Gurevich, Algebras of feasible functions, FOCS, pp.210-214, 1983.

T. Hagino, A typed lambda calculus with categorical type constructors, CTCS, vol.283, pp.140-57, 1987.

J. Hoffmann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, POPL, vol.46, pp.357-370, 2011.

J. Hoffmann, K. Aehlig, and M. Hofmann, Resource aware ML, CAV, pp.781-786, 2012.

P. Hajek, Arithmetical hierarchy and complexity of computation, Theoretical Computer Science, vol.8, issue.2, pp.227-237, 1979.

J. Hoffmann and M. Hofmann, Amortized resource analysis with polynomial potential, ESOP, pp.287-306, 2010.

M. Hofmann and S. Jost, Static prediction of heap space usage for firstorder functional programs, POPL, vol.38, pp.185-197, 2003.

M. Hofmann and S. Jost, Type-based amortised heap-space analysis, ESOP, pp.22-37, 2006.

M. Heizmann, N. Jones, and A. Podelski, Size-change termination and transition invariants, SAS, pp.22-50, 2010.

N. Hirokawa and G. Moser, Automated complexity analysis based on the dependency pair method, IJCAR, pp.364-379, 2008.

N. Hirokawa and G. Moser, Automated complexity analysis based on context-sensitive rewriting, TLCA and RTA, pp.257-271, 2014.

M. Hofmann and G. Moser, Amortised resource analysis and typed polynomial interpretations, TLCA and RTA, pp.272-286, 2014.

M. Hofmann and G. Moser, Multivariate amortised resource analysis for term rewrite systems, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.38, pp.241-256, 2015.

E. Hainry, J. Marion, and R. Péchoux, Type-based complexity analysis for fork processes, FoSSaCS, pp.305-320, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00755450

D. Hofbauer, Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Theoretical Computer Science, vol.105, issue.1, pp.129-140, 1992.

M. Hofmann, Linear types and non-size-increasing polynomial time computation, LICS, pp.464-473, 1999.

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.

D. Hofbauer, Termination proofs by context-dependent interpretations, RTA, pp.108-121, 2001.

M. Hofmann, The strength of non-size increasing computation, POPL, vol.37, issue.1, pp.260-269, 2002.

M. Hofmann, Linear types and non-size-increasing polynomial time computation. Information and Computation, vol.183, pp.57-85, 2003.

E. Hainry and R. Péchoux, Objects in polynomial time, APLAS, pp.387-404, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01206161

E. Hainry and R. Péchoux, Higher order interpretation for higher order complexity, LPAR, EPIC, pp.269-285, 2017.

E. Hainry and R. Péchoux, A type-based complexity analysis of object oriented programs. Information and Computation, vol.261, pp.78-115, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01712506

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, POPL, pp.410-423, 1996.

M. Hofmann and D. Rodriguez, Efficient type-checking for amortised heap-space analysis, CSL, pp.317-331, 2009.

M. Hofmann and D. Rodriguez, Automatic type inference for amortised heap-space analysis, ESOP, pp.593-613, 2013.

M. Hofmann, R. Ramyaa, and U. Schöpp, Pure pointer programs and tree isomorphism, FoSSaCS, pp.321-336, 2013.

M. Hofmann and U. Schöpp, Pure pointer programs with iteration, Transactions on Computational Logic, vol.11, issue.4, p.26, 2010.

J. Hoffmann and Z. Shao, Automatic static cost analysis for parallel programs, ESOP, pp.132-157, 2015.

D. Hofbauer and J. Waldmann, Termination of string rewriting with matrix interpretations, RTA, pp.328-342, 2006.

R. J. Irwin, B. M. Kapron, and J. S. Royer, On characterizations of the basic feasible functionals, Part II, 2002.

N. Immerman, Relational queries computable in polynomial time, Information and Control, vol.68, issue.1-3, pp.86-104, 1986.

N. Immerman, Descriptive Complexity, 2012.

A. Igarashi, B. C. Pierce, and P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ, Transactions on Programming Languages and Systems, vol.23, issue.3, pp.396-450, 2001.

R. J. Irwin, J. S. Royer, and B. M. Kapron, On characterizations of the basic feasible functionals, Part I, Journal of Functional Programming, vol.11, issue.1, pp.117-153, 2001.

P. Jacobé-de-naurois, Pointers in recursion: Exploring the tropics, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.1-18, 2019.

S. Jost, K. Hammond, H. Loidl, and M. Hofmann, Static determination of quantitative resource usage for higher-order programs, POPL, vol.45, pp.223-236, 2010.

N. Jones and L. Kristiansen, The flow of data and the complexity of algorithms, CIE, pp.263-274, 2005.

N. Jones and L. Kristiansen, A flow calculus of mwp-bounds for complexity analysis, Transactions on Computational Logic, vol.10, issue.4, p.28, 2009.

N. Jones, Logspace and Ptime characterized by programming languages. Theoretical Computer Science, vol.228, pp.151-174, 1999.

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.

B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.222-259, 1997.

J. W. Klop, Term Rewriting Systems, 2001.

L. Kalmár, Egyszerü példa eldönthetetlen aritmetikai problémára. Mate és fizikai lapok, vol.50, pp.1-23, 1943.

S. Kamin, Attempts for generalizing the recursive path orderings, 1980.

M. Bruce, S. A. Kapron, and . Cook, A new characterization of Mehlhorn's polynomial time functionals, FOCS, pp.342-347, 1991.

M. Bruce, S. A. Kapron, and . Cook, A new characterization of type-2 feasibility, SIAM Journal on Computing, vol.25, issue.1, pp.117-132, 1996.

N. Kobayashi, U. D. Lago, and C. Grellois, On the termination problem for probabilistic higher-order recursive programs, LICS, pp.1-14, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02399361

J. Benjamin-lucien-kaminski, C. Katoen, F. Matheja, and . Olmedo, Weakest precondition reasoning for expected runtimes of probabilistic programs, ESOP, pp.364-389, 2016.

S. Kleene, A theory of positive integers in formal logic. Part I, American Journal of Mathematics, vol.57, issue.1, pp.153-173, 1935.

S. Kleene, General recursive functions of natural numbers, Mathematische annalen, vol.112, issue.1, pp.727-742, 1936.

M. Krishnamoorthy and P. Narendran, On recursive path ordering, Theoretical Computer Science, vol.40, pp.323-328, 1985.

L. Kristiansen and K. Niggl, On the computational complexity of imperative programming languages, Theoretical Computer Science, vol.318, issue.1-2, pp.139-161, 2004.

-. Ker and . Ko, Complexity Theory of Real Functions. Birkhäuser, 1991.

M. Kurihara and A. Ohuchi, Modularity of simple termination of term rewriting systems with shared constructors, Theoretical Computer Science, vol.103, issue.2, pp.273-282, 1992.

D. Kozen, Semantics of probabilistic programs, SFCS, pp.101-114, 1979.

B. W. Kernighan and R. Pike, The Unix Programming Environment, 1984.

M. Bruce, F. Kapron, and . Steinberg, Type-two polynomial-time and restricted lookahead, LICS, pp.579-588, 2018.

M. Bruce, F. Kapron, O. Steinberg-;-rody-kersten, . Shkaravska, M. Bernard-van-gastel et al., Making resource analysis practical for real-time Java, Electronic Proceedings in Theoretical Computer Science, vol.298, pp.135-144, 2012.

L. Kristiansen and P. Voda, Complexity classes and fragments of C. Information Processing Letters, vol.88, pp.213-218, 2003.

D. Kesner and P. Vial, Types as resources for classical natural deduction, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.84, pp.1-17, 2017.

Y. Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004.

D. Lankford, On proving term rewriting systems are Noetherien, 1979.

C. Lautemann, A note on polynomial interpretation, Bulletin of the EATCS, vol.36, pp.129-130, 1988.

D. Leivant, Ramified recurrence and computational complexity I: Word recurrence and poly-time, Feasible mathematics, pp.320-343, 1995.

D. Leivant, A characterization of NC by tree recurrence, FOCS, pp.716-724, 1998.

N. Chin-soon-lee, A. Jones, and . Ben-amram, The size-change principle for program termination, POPL, vol.36, pp.81-92, 2001.

D. Leivant and J. Marion, Lambda calculus characterizations of polytime, TLCA, pp.274-288, 1993.

D. Leivant and J. Marion, Ramified recurrence and computational complexity II: substitution and poly-space, CSL, pp.486-500, 1994.

D. Leivant and J. Marion, A characterization of alternating log time by ramified recurrence, Theoretical Computer Science, vol.236, issue.1-2, pp.193-208, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099078

D. Leivant and J. Marion, Evolving graph-structures and their implicit computational complexity, ICALP, pp.349-360, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00939484

O. Laurent and L. Tortora-de-falco, Obsessional cliques: a semantic characterization of bounded time complexity, LICS, pp.179-188, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00096274

S. Lucas, Polynomials over the reals in proofs of termination: from theory to practice, RAIRO-Theoretical Informatics and Applications, vol.39, issue.3, pp.547-586, 2005.

S. Lucas, Practical use of polynomials over the reals in proofs of termination, PPDP, pp.39-50, 2007.

A. Madet and R. M. Amadio, An elementary affine ?-calculus with multithreading and side effects, TLCA, pp.138-152, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00610012

A. Madet, A polynomial time ?-calculus with multithreading and side effects, PPDP, pp.55-66, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00735544

J. Marion, A type system for complexity flow analysis, LICS, pp.123-132, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591853

F. Maurel, Nondeterministic light logics and NP-time, TLCA, pp.241-255, 2003.

D. Mazza, An infinitary affine lambda-calculus isomorphic to the full lambda-calculus, LICS, pp.471-480, 2012.

D. Mazza, Non-uniform polytime computation in the infinitary affine lambda-calculus, ICALP, pp.305-317, 2014.

D. Mazza, Simple parsimonious types and logarithmic space, CSL, volume 41 of LIPIcs, pp.24-40, 2015.

K. Mehlhorn, Polynomial and abstract subrecursive classes, Journal of Computer and System Sciences, vol.12, issue.2, pp.147-178, 1976.

J. , Y. Marion, and J. Moyen, Efficient first order functional program interpreter with time bound certifications, LPAR, pp.25-42, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099178

Z. Manna and S. Ness, On the termination of markov algorithms, HICSS, pp.789-792, 1970.

A. Murawski and L. Ong, On an interpretation of safe recursion in light affine logic, Theoretical Computer Science, vol.318, issue.1-2, pp.197-223, 2004.

J. Moyen, Resource control graphs. Transactions on Computational Logic, vol.10, issue.4, p.29, 2009.

J. , Y. Marion, and R. Péchoux, Resource analysis by sup-interpretation, FLOPS, pp.163-176, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000661

J. , Y. Marion, and R. Péchoux, Analyzing the implicit computational complexity of object-oriented programs, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.2, pp.316-327, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332550

J. , Y. Marion, and R. Péchoux, A characterization of NC k by first order functional programs, TAMC, pp.136-147, 2008.

J. , Y. Marion, and R. Péchoux, Characterizations of polynomial complexity classes with a better intensionality, PPDP, pp.79-88, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332389

J. , Y. Marion, and R. Péchoux, Sup-interpretations, a semantic method for static analysis of program resources, Transactions on Computational Logic, vol.10, issue.4, p.27, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00446057

J. , Y. Marion, and R. Péchoux, Complexity information flow in a multithreaded imperative language, TAMC, pp.124-140, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00684026

G. Moser and A. Schnabl, Proving quadratic derivational complexities using context dependent interpretations, RTA, pp.276-290, 2008.

G. Moser and A. Schnabl, The derivational complexity induced by the dependency pair method, RTA, pp.255-269, 2009.

G. Moser and A. Schnabl, Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.10, pp.235-250, 2011.

G. Moser, A. Schnabl, and J. Waldmann, Complexity analysis of term rewriting based on matrix and context dependent interpretations, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.2, pp.304-315, 2008.

D. Mazza and K. Terui, Parsimonious types and non-uniform computation, ICALP, pp.350-361, 2015.

H. Müller, Klassifizierungen der primitiv-rekursiven Funktionen, 1974.

Q. Van-chan-ngo, J. Carbonneaux, and . Hoffmann, Bounded expectations: resource analysis for probabilistic programs, PLDI, vol.53, pp.496-512

L. Noschinski, F. Emmes, and J. Giesl, Analyzing innermost runtime complexity of term rewriting by dependency pairs, Journal of Automated Reasoning, vol.51, issue.1, pp.27-56, 2013.

K. Niggl, The µ-measure as a tool for classifying computational complexity, Archive for Mathematical Logic, vol.39, issue.7, pp.515-539, 2000.

F. Neurauter and A. Middeldorp, Polynomial interpretations over the reals do not subsume polynomial interpretations over the integers, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, pp.243-258, 2010.

K. Niggl and H. Wunderlich, Certifying polynomial time and linear/polynomial space for imperative programs, SIAM Journal on Computing, vol.35, issue.5, pp.1122-1147, 2006.

F. Neurauter, H. Zankl, and A. Middeldorp, Revisiting matrix interpretations for polynomial derivational complexity of term rewriting, LPAR, pp.550-564, 2010.

I. Oitavem, Implicit characterizations of PSPACE, PTCS, pp.170-190

. Springer, , 2001.

, Christos Papadimitriou. Computational Complexity, 2003.

R. Péchoux, Synthesis of sup-interpretations: a survey, Theoretical Computer Science, vol.467, pp.30-52, 2013.

S. Perdrix, Quantum entanglement analysis based on abstract interpretation, SAS, pp.270-282, 2008.

M. Perrinel, Paths-based criteria and application to linear logic subsystems characterizing polynomial time, Information and Computation, vol.261, pp.23-54, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02154716

R. Péter, Recursive Functions, 1967.

C. Benjamin and . Pierce, Basic Category Theory for Computer Scientists, 1991.

C. Benjamin and . Pierce, Types and Programming Languages, 2002.

F. Pitt, A quantifier-free theory based on a string algebra for NC 1, Proof complexity and feasible arithmetics, pp.229-252, 1998.

D. Plaisted, A recursively defined ordering for proving termination of term rewriting systems, 1978.

A. Podelski and A. Rybalchenko, Transition invariants, LICS, pp.32-41, 2004.

B. F. Redmond, Multiplexor categories and models of soft linear logic, LFCS, pp.472-485, 2007.

O. Reingold, Undirected connectivity in log-space, Journal of the ACM, vol.55, issue.4, p.17, 2008.

J. C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, vol.2, pp.717-740

J. C. Reynolds, Towards a theory of type structure, Programming Symposium, pp.408-425, 1974.

R. Ritchie, Classes of predictably computable functions, Transactions of the American Mathematical Society, vol.106, issue.1, pp.139-173, 1963.

H. Rose, Subrecursion: Functions and Hierarchies, 1987.

L. Roversi, A p-time completeness proof for light logics, CSL, pp.469-483

. Springer, , 1999.

L. Walter and . Ruzzo, On uniform circuit complexity, Journal of Computer and System Sciences, vol.22, issue.3, pp.365-383, 1981.

D. Sands, Complexity analysis for a lazy higher-order language, ESOP, pp.361-376, 1990.

D. Sands, Time analysis, cost equivalence and program refinement, FSTTCS, pp.25-39, 1991.

J. E. Savage, Models of Computation, vol.136, 1998.

V. Sazonov, Polynomial computability and recursivity in finite domains, Elektronische Informationsverarbeitung und Kybernetik, vol.16, issue.7, pp.319-323, 1980.

H. Schwichtenberg, Rekursionszahlen und die Grzegorczyk-Hierarchie, Archiv für mathematische Logik und Grundlagenforschung, vol.12, issue.1-2, pp.85-97, 1969.

U. Schöpp, Stratified bounded affine logic for logarithmic space, LICS, vol.7, pp.411-420, 2007.

P. Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science, vol.14, issue.4, pp.527-586, 2004.

P. Severi, A light modality for recursion, FoSSaCS, pp.499-516, 2017.

W. Peter and . Shor, Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer, SIAM Journal on Computing, vol.26, issue.5, pp.1484-1509, 1997.

A. Ben and . Sijtsma, On the productivity of recursive list definitions, Transactions on Programming Languages and Systems, vol.11, issue.4, pp.633-649, 1989.

M. Sipser, Introduction to the Theory of Computation, Thomson Course Technology, 2006.

O. Shkaravska, R. Kersten, and M. C. Van-eekelen, Test-based inference of polynomial loop-bound functions, PPDP, pp.99-108, 2010.

A. Sabelfeld and D. Sands, Dimensions and principles of declassification, CSFW, pp.255-269, 2005.

J. Steinbach, Proving polynomials positive, FSTTCS, pp.191-202

. Springer, , 1992.

G. Smith and D. Volpano, Secure information flow in a multi-threaded imperative language, POPL, pp.355-364, 1998.

P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control, Mathematical Structures in Computer Science, vol.16, issue.3, pp.527-552, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00483924

O. Shkaravska, C. J. Marko, A. Van-eekelen, and . Tamalet, Collected size semantics for strict functional programs over general polymorphic lists, FOPARA, pp.143-159, 2013.

O. Shkaravska, C. J. Marko, R. Van-eekelen, and . Van-kesteren, Polynomial size analysis of first-order shapely functions, Logical Methods in Computer Science, vol.5, issue.2, 2009.

O. Shkaravska, R. Van-kesteren, and M. C. Van-eekelen, Polynomial size analysis of first-order functions, TLCA, pp.351-365, 2007.

D. Sangiorgi and D. Walker, The Pi-calculus: a Theory of Mobile Processes, 2003.

A. Tarski, A Decision Method for Elementary Algebra and Geometry, 1951.

K. Terui, Light affine lambda calculus and polytime strong normalization, LICS, pp.209-220, 2001.

M. Vardi, The complexity of relational query languages, STOC, pp.137-146, 1982.

P. Vasconcelos, Space cost analysis using sized types, 2008.

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2/3, pp.167-188, 1996.

P. Vasconcelos, S. Jost, M. Florido, and K. Hammond, Type-based allocation analysis for co-recursion in lazy functional languages, ESOP, pp.787-811, 2015.

H. Vollmer and K. Wagner, Recursion theoretic characterizations of complexity classes of counting functions, Theoretical Computer Science, vol.163, issue.1-2, pp.245-258, 1996.

J. Waldmann, Polynomially bounded matrix interpretations, of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, 2010.

J. Waldmann, Matrix interpretations on polyhedral domains, RTA, vol.36, 2015.

A. Weiermann, Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science, vol.139, issue.1-2, pp.355-362, 1995.

K. Weihrauch, Computable Analysis: An Introduction, 2000.

G. Winskel, The Formal Semantics of Programming Languages: An Introduction, 1993.

C. Gavin and . Wraith, A note on categorical datatypes, CTCS, vol.389, pp.118-127, 1993.

T. Yamada, Confluence and termination of simply typed term rewriting systems, RTA, pp.338-352, 2001.

T. Yamakami, A schematic definition of quantum polynomial time computability, 2018.

, Complexity