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. Chin and S. Khoo, Calculating Sized Types, Higher-Order and Symbolic Computation, vol.14, issue.2/3, pp.261-300, 2001.
DOI : 10.1023/A:1012996816178

J. Hannan, P. Hicks, and D. Liben-nowell, A Lifetime Analysis for Higher- Order Languages The Pennsylvania State University, 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. 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.

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

U. Dal, L. , 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

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

[. 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

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

T. Petricek, D. Orchard, and A. Mycroft, Coeffects: The Essence of Context Dependence, 2012.

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

[. Stampoulis and Z. Shao, Static and User-Extensible Proof Checking, 39th Symp. on Principles of Programming Languages (POPL'12), pp.273-284, 2012.