N. D. Jones, LOGSPACE and PTIME characterized by programming languages, Theoretical Computer Science, vol.228, issue.1-2, pp.151-174, 1999.
DOI : 10.1016/S0304-3975(98)00357-0

S. Cook, Characterizations of Pushdown Machines in Terms of Time-Bounded Computers, Journal of the ACM, vol.18, issue.1, pp.4-18, 1971.
DOI : 10.1145/321623.321625

P. Wadler, Deforestation: Transforming programs to eliminate trees, ESOP '88. European Symposium on Programming, pp.344-358, 1988.
DOI : 10.1007/3-540-19027-9_23

J. Y. Marion and J. Y. Moyen, Efficient first order functional program interpreter with time bound certifications, Lecture Notes in Computer Science, pp.25-42, 1955.
URL : https://hal.archives-ouvertes.fr/inria-00099178

G. Bonfante, J. Y. Marion, and J. Y. Moyen, On Lexicographic Termination Ordering with Space Bound Certifications, PSI 2001, Ershov Memorial Conference, 2001.
DOI : 10.1007/3-540-45575-2_46
URL : https://hal.archives-ouvertes.fr/inria-00100523

G. Bonfante, J. Y. Marion, and J. Y. Moyen, Quasi-interpretations and Small Space Bounds, Rewrite Techniques and Applications, pp.150-164, 2005.
DOI : 10.1007/978-3-540-32033-3_12
URL : https://hal.archives-ouvertes.fr/inria-00001234

S. Bellantoni and S. Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.106, issue.2, pp.97-110, 1992.
DOI : 10.1007/BF01201998

D. Leivant and J. Y. Marion, Lambda calculus characterizations of poly-time, Fundamenta Informaticae, vol.19, issue.167, p.184, 1993.
DOI : 10.1007/BFb0037112

D. Leivant and J. Y. Marion, Predicative functional recurrence and poly-space, TAPSOFT'97, pp.369-380, 1997.
DOI : 10.1007/BFb0030611

D. Leivant and J. Y. Marion, A characterization of alternating log time by ramified recurrence, Theoretical Computer Science, vol.236, issue.1-2, pp.192-208, 2000.
DOI : 10.1016/S0304-3975(99)00209-1
URL : https://hal.archives-ouvertes.fr/inria-00099078

P. Neergaard, A Functional Language for Logarithmic Space, Proc. 2nd Asian Symp. on Prog. Lang. and Systems, 2004.
DOI : 10.1007/978-3-540-30477-7_21

M. Hofmann, Linear types and non-size-increasing polynomial time computation, Proceedings of the Fourteenth IEEE Symposium on Logic in Computer Science (LICS'99, pp.464-473, 1999.

M. Hofmann, The strength of non size-increasing computation, POPL'02, pp.260-269, 2002.

P. Baillot and K. Terui, Light types for polynomial time computation in lambdacalculus, Proceedings, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00012752

I. Oitavem, A term rewriting characterization of the functions computable in polynomial space, Archive for Mathematical Logic, vol.41, issue.1, pp.35-47, 2002.
DOI : 10.1007/s001530200002

N. D. Jones, Computability and Complexity from a Programming Perspective, 1997.
DOI : 10.1007/978-94-010-0413-8_4

E. Grädel and Y. Gurevich, Abstract, The Journal of Symbolic Logic, vol.57, issue.03, pp.952-969, 1995.
DOI : 10.1016/0304-3975(92)90149-A