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

R. M. Amadio and Y. Régis-gianas, Certifying and Reasoning on Cost Annotations of Functional Programs, p.2350, 1110.
DOI : 10.1007/978-3-642-32495-6_5

J. W. De-bakker, Mathematical Theory of Program Correctness, 1980.

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.544.847

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

URL : http://doi.org/10.1016/j.tcs.2003.10.022

F. Bobot, J. C. Filliatre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

E. M. Clarke, Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM, vol.26, issue.1, pp.129-147, 1979.
DOI : 10.1145/322108.322121

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Mart´i-oliet et al., The Maude 2.0 System, RTA 2003, pp.76-87, 2003.
DOI : 10.1007/3-540-44881-0_7

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

D. Lago and U. , Context semantics, linear logic, and computational complexity, ACM Transactions on Computational Logic, vol.10, issue.4, pp.169-178, 2006.
DOI : 10.1145/1555746.1555749

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

D. Lago, U. Gaboardi, and M. , Linear dependent types and relative completeness, pp.133-142, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00906347

D. Lago, U. Petit, and B. , The geometry of types (long version), p.6857, 1210.

D. Lago, U. Petit, and B. , Linear dependent types in a call-by-value scenario, ACM PPDP 2012, pp.115-126, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00909371

V. Danos and L. Regnier, Reversible, irreversible and optimal ??-machines, Theoretical Computer Science, vol.227, issue.1-2, pp.79-97, 1999.
DOI : 10.1016/S0304-3975(99)00049-3

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

M. Felleisen and D. P. Friedman, Control operators, the SECD-machine and the ?-calculus, Tech. Rep, vol.197, 1986.

D. R. Ghica, Slot games: a quantitative model of computation, ACM POPL 2005, pp.85-97, 2005.

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

J. Y. 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

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.7406

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996.
DOI : 10.1145/237721.240882

S. Jost, K. Hammond, H. W. Loid, and M. Hofmann, Static determination of quantitative resource usage for higher-order programs, 2010.

J. L. Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, pp.199-207, 2007.
DOI : 10.1007/s10990-007-9018-9

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

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

G. D. Plotkin, LCF considerd as a programming language, Theor. Comp. Sci, vol.5, pp.225-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5

URL : http://doi.org/10.1016/0304-3975(77)90044-5

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

D. Sands, Operational theories of improvement in functional languages (extended abstract) In: Functional Programming, pp.298-311, 1991.

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The worst-case execution-time problem???overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems, vol.7, issue.3
DOI : 10.1145/1347375.1347389