B. Aspvall, M. F. Plass, and R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Inform. Process. Lett, vol.8, issue.79, pp.90002-90006, 1979.

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

P. Baillot and D. Mazza, Linear logic by levels and bounded time complexity, Theor. Comput. Sci, vol.411, pp.470-503, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00488531

P. Baillot and K. Terui, Light Types for Polynomial Time Computation in Lambda-Calculus, Logic in Computer Science, LICS, pp.266-275, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00012752

S. Bellantoni and S. Cook, A New Recursion-Theoretic Characterization of the Polytime Functions, Computational Complexity, vol.2, pp.97-110, 1992.

M. Amir, N. D. Ben-amram, L. Jones, and . Kristiansen, Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time, Logic and Theory of Algorithms, pp.67-76, 2008.

G. Bonfante, J. Marion, and J. Moyen, Quasiinterpretations a way to control resources, Theor. Comput. Sci, vol.412, pp.2776-2796, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591862

A. Cobham, The intrinsic computational difficulty of functions, Proceedings of the International Conference on Logic, pp.24-30, 1965.

L. Robert and . Constable, Type two computational complexity, Proc. 5th annual ACM Symposium on Theory of Computing, pp.108-121, 1973.

B. Cook, A. Podelski, and A. Rybalchenko, TERMI-NATOR: beyond safety, International Conference on Computer Aided Verification, pp.415-418, 2006.

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

A. Stephen, B. M. Cook, and . Kapron, Characterizations of the basic feasible functionals of finite type, 30th Annual Symposium on Foundations of Computer Science (FOCS 1989), pp.154-159, 1989.

A. Stephen, A. Cook, and . Urquhart, Functional interpretations of feasibly constructive arithmetic, Ann. Pure Appl. Logic, vol.63, pp.103-200, 1993.

N. Danner and J. S. Royer, Adventures in time and space, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.168-179, 2006.

S. Even, A. Itai, and A. Shamir, On the Complexity of Timetable and Multicommodity Flow Problems, SIAM J. Comput, vol.5, pp.691-703, 1976.

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

M. Gaboardi, J. Marion, and S. Rocca, A logical account of pspace, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.121-131, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00342323

J. Girard, Light Linear Logic, Inf. Comput, vol.143, pp.175-204, 1998.

E. Hainry, J. Marion, and R. Péchoux, Typebased complexity analysis for fork processes, International Conference on Foundations of Software Science and Computational Structures, pp.305-320, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00755450

E. Hainry and R. Péchoux, Objects in Polynomial Time, Programming Languages and Systems -13th Asian Symposium, APLAS 2015 (Lecture Notes in Computer Science), 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-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, pp.269-285, 2017.

P. Hájek, Arithmetical Hierarchy and Complexity of Computation. Theor. Comput. Sci, vol.8, pp.227-237, 1979.

R. J. Irwin, J. S. Royer, and B. M. Kapron, On characterizations of the basic feasible functionals (Part I), J. Funct. Program, vol.11, pp.117-153, 2001.

D. Neil, L. Jones, and . Kristiansen, A Flow Calculus of Mwp-bounds for Complexity Analysis, ACM Trans. Comput. Logic, vol.10, p.41, 2009.

M. Bruce, S. A. Kapron, and . Cook, A New Characterization of Mehlhorn's Polynomial Time Functionals (Extended Abstract), 32nd Annual Symposium on Foundations of Computer Science, pp.342-347, 1991.

M. Bruce, S. A. Kapron, and . Cook, A New Characterization of Type-2 Feasibility, SIAM J. Comput, vol.25, pp.117-132, 1996.

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

M. Bruce, F. Kapron, and . Steinberg, Type-two iteration with bounded query revision, Proceedings Third Joint Workshop on Developments in Implicit Computational complExity and Foundational & Practical Aspects of Resource Analysis, DICE-FOPARA@ETAPS 2019 (EPTCS), pp.61-73, 2019.

A. Kawamura and F. Steinberg, Polynomial Running Times for Polynomial-Time Oracle Machines, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.23, pp.1-23, 2017.

N. D. Chin-soon-lee, A. M. Jones, and . Ben-amram, The sizechange principle for program termination, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.81-92, 2001.

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

D. Leivant and J. Marion, Evolving Graph-Structures and Their Implicit Computational Complexity, Automata, Languages, and Programming -40th International Colloquium, ICALP 2013, Proceedings, Part II, pp.349-360, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00939484

D. Leivant and J. Marion, Lambda Calculus Characterizations of Poly-Time, Fundam. Inform, vol.19, issue.2, pp.167-184, 1993.

J. Marion, A Type System for Complexity Flow Analysis, Logic in Computer Science, LICS 2011, pp.123-132, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591853

J. , Y. Marion, and R. Péchoux, Complexity Information Flow in a Multi-threaded Imperative Language, Theory and Applications of Models of Computation, TAMC 2014, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00684026

. Springer, , pp.124-140

K. Mehlhorn, Polynomial and abstract subrecursive classes, J. Comp. Sys. Sci, vol.12, issue.76, pp.80035-80044, 1976.

C. John and . Mitchell, Type inference with simple subtypes, J. Funct. Program, vol.1, pp.245-285, 1991.

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of computer security, vol.4, pp.167-187, 1996.