Z. Manna and S. Ness, On the termination of Markov algorithms, Third hawaii international conference on system science, pp.789-792, 1970.

D. Lankford, On proving term rewriting systems are noetherien. tech. rep, 1979.

P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static 395 analysis of programs by construction or approximation of fixpoints, Proceedings of ACM POPL, pp.77-238, 1977.

G. Bonfante, J. Y. Marion, and J. Y. Moyen, Quasi-interpretations a way to control resources, Theoretical Computer Science, vol.412, issue.25
DOI : 10.1016/j.tcs.2011.02.007
URL : https://hal.archives-ouvertes.fr/hal-00591862

R. Amadio, Synthesis of max-plus quasi-interpretations. Fundamenta Informati- 400 cae, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00146968

J. Y. Marion and R. Péchoux, Sup-interpretations, a semantic method for static analysis of program resources, ACM Transactions on Computational Logic, vol.10, issue.4, 2009.
DOI : 10.1145/1555746.1555751
URL : https://hal.archives-ouvertes.fr/inria-00446057

J. Y. Marion and R. Péchoux, A Characterization of NCk by First Order Functional Programs, LNCS, vol.4978, p.136, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332390

G. Bonfante, R. Kahle, J. Y. Marion, and I. Oitavem, Recursion Schemata for NC k, LNCS, vol.5213, pp.49-63, 2008.
DOI : 10.1007/978-3-540-87531-4_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.9971

E. W. Dijkstra, On the productivity of recursive definitions, pp.749-410, 1980.

B. Sijtsma, On the productivity of recursive list definitions, ACM Transactions on Programming Languages and Systems, vol.11, issue.4, pp.633-649, 1989.
DOI : 10.1145/69558.69563

T. Coquand, Infinite objects in type theory, LNCS, vol.806, pp.62-78, 1994.
DOI : 10.1007/3-540-58085-9_72

W. Wadge, An extensional treatment of dataflow deadlock, Theoretical Computer Science, vol.13, issue.1, pp.3-15, 1981.
DOI : 10.1016/0304-3975(81)90108-0

A. Telford and D. Turner, Ensuring streams flow, LNCS, vol.1349, pp.509-523, 1997.
DOI : 10.1007/BFb0000493

W. Buchholz, A term calculus for (co-)recursive definitions on streamlike data structures, Annals of Pure and Applied Logic, vol.136, issue.1-2, pp.75-90, 2005.
DOI : 10.1016/j.apal.2005.05.006

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using 420 sized types, Proceedings of ACM POPL'96, pp.410-423, 1996.

S. Frankau and A. Mycroft, Stream processing hardware from functional language specifications. Proceeding of IEEE, p.36, 2003.
DOI : 10.1109/hicss.2003.1174809
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.5058

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

J. Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.144-154, 1993.
DOI : 10.1145/158511.158618

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.404.4058

J. Y. Marion and R. Péchoux, Characterizations of polynomial complexity classes with a better intensionality, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.79-88, 2008.
DOI : 10.1145/1389449.1389460
URL : https://hal.archives-ouvertes.fr/inria-00332389

R. Bird and P. Wadler, Introduction to Functional Programming, 1988.