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
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
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
Type-Based Termination with Sized Products, LNCS, vol.5213, pp.493-507, 2008. ,
DOI : 10.1007/978-3-540-87531-4_35
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
Resource bound certification, pp.184-198, 2000. ,
Static Determination of Quantitative Resource Usage for Higher-Order Programs, pp.223-236, 2010. ,
Linear types and non-size-increasing polynomial time computation, pp.464-473, 1999. ,
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
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
Dependent types for program termination verification, pp.231-246, 2001. ,
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
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
Execution time of lambda-terms via denotational semantics and intersection types, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00319822
A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, pp.199-207, 2007. ,
Control Operators, the SECD-Machine and the ?-Calculus, 1986. ,
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
Bounded linear logic: A modular approach to polynomial-time computability, Theor. Comput. Sci, pp.97-98, 1992. ,
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
Parallel Beta Reduction Is Not Elementary Recursive, Information and Computation, vol.170, issue.1, pp.49-80, 2001. ,
DOI : 10.1006/inco.2001.2869
The Optimal Implementation of Functional Programming Languages, 1998. ,
Classical Recursion Theory: the Theory of Functions and Sets of Natural Numbers, number 125 in Studies in Logic and the Foundations of Mathematics, 1989. ,
Term Rewriting and All That, 1998. ,
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
Linear Dependent Types and Relative Completeness, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2012. ,
DOI : 10.1109/LICS.2011.22
The geometry of types, pp.167-178, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00909318
Mathematical theory of program correctness, Prentice-Hall international series in computer science, 1980. ,
Complexity analysis for a lazy higher-order language, LNCS, vol.432, pp.361-376, 1990. ,
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
A static cost analysis for a higherorder language, pp.25-34, 2013. ,
Régis-Gianas, Certifying and reasoning on cost annotations in c programs, pp.32-46 ,
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
SPEED: Symbolic Complexity Bound Analysis, LNCS, vol.5643, pp.51-62, 2009. ,
DOI : 10.1007/978-3-642-02658-4_7
Geometry of synthesis III: resource management through type inference, pp.345-356, 2011. ,