. .. Tn{au, I m ? J m ; 3. for every 1 ? p ? m, both ?; H $ U I p tn{au » I n p and ? p ; 4. for every n P N, it holds that ?, J n, vol.1, issue.1

S. Abramsky, R. Jagadeesan, and P. Malacaria, Full abstraction for PCF. I & C, pp.409-470, 2000.

K. R. Apt, F. S. De-boer, and E. Olderog, Verification of Sequential and Concurrent Programs, Comp. Sci, 2009.

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

P. Baillot, M. Gaboardi, and V. Mogbil, A PolyTime Functional Language from Light Linear Logic, ESOP, pp.104-124, 2010.
DOI : 10.1007/978-3-642-11957-6_7
URL : https://hal.archives-ouvertes.fr/hal-00443944

P. Baillot and K. Terui, Light types for polynomial time computation in lambda calculus. I & C, pp.41-62, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00012752

G. Barthe, B. Grégoire, and C. Riba, Type-Based Termination with Sized Products, CSL, pp.493-507, 2008.
DOI : 10.1007/978-3-540-87531-4_35

A. Bernadet and S. Lengrand, Complexity of Strongly Normalising ??-Terms via Non-idempotent Intersection Types, FOSSACS, pp.88-107, 2011.
DOI : 10.1007/978-3-642-19805-2_7
URL : https://hal.archives-ouvertes.fr/hal-01110489

A. Bucciarelli, S. D. Lorenzis, A. Piperno, and I. Salvo, Some computational properties of intersection types, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.109-118, 1999.
DOI : 10.1109/LICS.1999.782598

A. Bucciarelli, A. Piperno, and I. Salvo, Intersection types and lambda-definability, MSCS, vol.13, issue.1, pp.15-53, 2003.

S. A. Cook, Soundness and Completeness of an Axiom System for Program Verification, SIAM Journal on Computing, vol.7, issue.1, pp.70-90, 1978.
DOI : 10.1137/0207005

K. Crary and S. Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.184-198, 2000.
DOI : 10.1145/325694.325716

U. and D. Lago, Context semantics, linear logic, and computational complexity, ACM Transactions on Computational Logic, vol.10, issue.4, 2009.
DOI : 10.1145/1555746.1555749
URL : https://hal.archives-ouvertes.fr/hal-00088823

U. , D. Lago, and M. Hofmann, Bounded linear logic, revisited, LMCS, vol.6, issue.4, 2010.

D. De-carvalho, Execution time of lambda-terms via denotational semantics and intersection types, p.4251, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00319822

E. Denney, Refinement types for specification, IFIP-PROCOMET, pp.148-166, 1998.
DOI : 10.1007/978-0-387-35358-6_13

M. Dezani-ciancaglini, E. Giovannetti, and U. De-'liguoro, Intersection Types, Lambda-models and Böhm Trees, Theories of Types and Proofs, pp.45-97, 1998.

T. Freeman and F. Pfenning, Refinement types for ML, PLDI, pp.268-277, 1991.

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, 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.
DOI : 10.1016/0304-3975(92)90386-T

B. Grobauer, Cost recurrences for DML programs, ICFP, pp.253-264, 2001.

C. A. Gunter, Semantics of Programming Languages: Structures and Techniques, Found. of Comp. Series, 1992.

J. Hoffmann, K. Aehlig, and M. Hofmann, Multivariate Amortized Resource Analysis, ACM POPL, pp.357-370, 2011.

M. Hofmann, Linear types and non-size-increasing polynomial time computation, LICS, pp.464-473, 1999.
DOI : 10.1109/lics.1999.782641
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.216

M. Hofmann, Programming languages capturing complexity classes, ACM SIGACT News, vol.31, issue.1, pp.31-42, 2000.
DOI : 10.1145/346048.346051

S. Jost, K. Hammond, H. Loid, and M. Hofmann, Static Determination of Quantitative Resource Usage for Higher-Order Programs, ACM POPL, 2010.

N. Kobayashi and C. L. Ong, A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes, 2009 24th Annual IEEE Symposium on Logic In Computer Science, pp.179-188, 2009.
DOI : 10.1109/LICS.2009.29

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

D. Leivant, Discrete polymorphism, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.288-297, 1990.
DOI : 10.1145/91556.91675

J. Marion, Complexité implicite des calculs, de la théoriè a la pratique, 2000.

P. Odifreddi, Classical Recursion Theory: the Theory of Functions and Sets of Natural Numbers, Number 125 in Studies in Logic and the Foundations of Mathematics, 1989.

G. D. Plotkin, LCF considerd as a programming language, Theor. Comp. Sci, vol.5, pp.225-255, 1977.

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003.
DOI : 10.1109/JSAC.2002.806121

D. M. Volpano, C. E. 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.
DOI : 10.3233/JCS-1996-42-304

H. Xi, Dependent types for program termination verification, LICS, pp.231-246, 2001.

H. Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, vol.17, issue.02, pp.215-286, 2007.
DOI : 10.1017/S0956796806006216

H. Xi and F. Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.214-227, 1999.
DOI : 10.1145/292540.292560