A. Abel, Semi-continuous Sized Types and Termination, Log. Methods Comput. Sci, vol.4, issue.2, 2008.

G. Barthe, B. Grégoire, and C. Riba, Type-Based Termination with Sized Products, Computer Science Logic, 17th Ann. Conf. (CSL'08, pp.493-507, 2008.
DOI : 10.1007/978-3-540-87531-4_35

W. N. Chin and S. C. Khoo, Calculating Sized Types, High.-Ord. and Symb, pp.261-300, 2001.
DOI : 10.1145/328690.328893
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.4005

J. Hannan, P. Hicks, and D. Liben-nowell, A Lifetime Analysis for Higher-Order Languages The Pennsylvania State University, Tech. rep, 1997.

N. Heintze and J. G. Riecke, The SLam calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.365-377, 1998.
DOI : 10.1145/268946.268976

S. Jost, K. Hammond, H. W. Loidl, and M. Hofmann, Static Determination of Quantitative Resource Usage for Higher-Order Programs, 37th Symp. on Principles of Programming Languages (POPL'10, pp.223-236, 2010.

U. D. Lago and B. Petit, The Geometry of Types, 40th Symp. on Principles of Programming Languages (POPL'13, pp.167-178, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909318

X. Leroy, Polymorphic Typing of an Algorithmic Language, Research report, vol.1778, 1992.
URL : https://hal.archives-ouvertes.fr/inria-00077018

Y. Minamide, J. G. Morrisett, and R. Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.271-283, 1996.
DOI : 10.1145/237721.237791
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.141.7192

E. Moggi, W. Taha, . Benaissa, and T. Sheard, An Idealized MetaML: Simpler, and More Expressive, 8th Europ. Symp. on Programming (ESOP'99, pp.193-207, 1999.
DOI : 10.1007/3-540-49099-X_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.1131

A. Nanevski, F. Pfenning, and B. Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.
DOI : 10.1145/1352582.1352591
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796

T. Petricek, D. Orchard, and A. Mycroft, Coeffects: Unified static analysis of contextdependence, Automata, Languages, and Programming -40th Int. Colloq. (ICALP'13, pp.385-397, 2013.

B. Pientka and J. Dunfield, Programming with proofs and explicit contexts, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.163-173, 2008.
DOI : 10.1145/1389449.1389469

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.3979

A. Stampoulis and Z. Shao, Static and User-Extensible Proof Checking, 39th Symp. on Principles of Programming Languages (POPL'12, pp.273-284, 2012.
DOI : 10.1145/2103656.2103690
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.232.7615

T. Tsukada and A. Igarashi, A Logical Foundation for Environment Classifiers, Logical Methods in Computer Science, vol.6, issue.4, 2010.