U. Dal-lago and M. Gaboardi, Linear Dependent Types and Relative Completeness, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp.133-142, 2011.
DOI : 10.1109/LICS.2011.22

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

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

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

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

S. Karlbary and . Weirich, Resource bound certification, pp.184-198, 2000.

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

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

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.
DOI : 10.1016/j.ic.2008.08.005
URL : https://hal.archives-ouvertes.fr/hal-00012752

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

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

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

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

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

J. Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, pp.199-207, 2007.

M. Felleisen and D. P. Friedman, Control Operators, the SECD-Machine and the ?-Calculus, 1986.

J. Maraist, M. Odersky, D. N. Turner, and P. Wadler, Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus, Electronic Notes in Theoretical Computer Science, vol.1, pp.370-392, 1995.
DOI : 10.1016/S1571-0661(04)00022-2

J. Girard, A. Scedrov, and P. J. Scott, Bounded linear logic: A modular approach to polynomial-time computability, Theor. Comput. Sci, pp.97-98, 1992.

J. Lamping, An algorithm for optimal lambda calculus reduction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.16-30, 1990.
DOI : 10.1145/96709.96711

A. Asperti and H. G. Mairson, Parallel Beta Reduction Is Not Elementary Recursive, Information and Computation, vol.170, issue.1, pp.49-80, 2001.
DOI : 10.1006/inco.2001.2869

A. Asperti and S. Guerrini, The Optimal Implementation of Functional Programming Languages, 1998.

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.

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

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

U. Dal-lago and M. Gaboardi, Linear Dependent Types and Relative Completeness, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2011.22

U. Dal-lago and B. Petit, The geometry of types, pp.167-178, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909318

J. W. De-bakker, A. De-bruin, and J. Zucker, Mathematical theory of program correctness, Prentice-Hall international series in computer science, 1980.

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

R. Benzinger, Automated higher-order complexity analysis, Theoretical Computer Science, vol.318, issue.1-2, pp.79-103, 2004.
DOI : 10.1016/j.tcs.2003.10.022

N. Danner, J. Paykin, and J. S. Royer, A static cost analysis for a higherorder language, pp.25-34, 2013.

N. Ayache, R. M. Amadio, and Y. , Régis-Gianas, Certifying and reasoning on cost annotations in c programs, pp.32-46

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

S. Gulwani, SPEED: Symbolic Complexity Bound Analysis, LNCS, vol.5643, pp.51-62, 2009.
DOI : 10.1007/978-3-642-02658-4_7

D. R. Ghica and A. Smith, Geometry of synthesis III: resource management through type inference, pp.345-356, 2011.