A. Abel, Mixed Inductive/Coinductive Types and Strong Normalization, APLAS, pp.286-301, 2007.
DOI : 10.1007/978-3-540-76637-7_19

S. Abramsky, R. Jagadeesan, and P. Malacaria, Full Abstraction for PCF, Information and Computation, vol.163, issue.2, pp.409-470, 2000.
DOI : 10.1006/inco.2000.2930

P. Baillot and K. Terui, 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

H. Barendregt, The Lambda Calculus, Its Syntax and Semantics, 1980.

H. Barendregt and J. W. Klop, Applications of infinitary lambda calculus, Information and Computation, vol.207, issue.5, pp.559-582, 2009.
DOI : 10.1016/j.ic.2008.09.003

A. Cave, F. Ferreira, P. Panangaden, and B. Pientka, Fair reactive programming, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.361-372, 2014.
DOI : 10.1145/2535838.2535881

U. , D. Lago, and M. Gaboardi, Linear dependent types and relative completeness, LICS, pp.133-142, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00906347

V. Danos and J. Joinet, Linear logic and elementary time, Information and Computation, vol.183, issue.1, pp.123-137, 2003.
DOI : 10.1016/S0890-5401(03)00010-5

E. W. Dijkstra, On the productivity of recursive definitions. Personal note EWD 749 Available at http://www.cs.utexas, 1980.

J. Endrullis and A. Polonsky, Infinitary rewriting coinductively, TYPES, pp.16-27, 2011.

M. Gaboardi and S. Rocca, A soft type assignment system for lambda -calculus, CSL, pp.253-267, 2007.

J. Girard, A. Scedrov, and P. J. Scott, Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, vol.97, issue.1, pp.1-66, 1992.
DOI : 10.1016/0304-3975(92)90386-T

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Geometry of Interaction 1: Interpretation of System F, Proceedings of the Logic Colloquium '88, pp.221-260, 1989.
DOI : 10.1016/S0049-237X(08)70271-4

J. Girard, Light Linear Logic, Information and Computation, vol.143, issue.2, pp.175-204, 1998.
DOI : 10.1006/inco.1998.2700

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996.
DOI : 10.1145/237721.240882

R. Kennaway, J. W. Klop, M. R. Sleep, and F. Vries, Transfinite reductions in orthogonal term rewriting systems, RTA, pp.1-12, 1991.

R. Kennaway, J. W. Klop, M. R. Sleep, and F. Vries, Infinitary lambda calculus, Theoretical Computer Science, vol.175, issue.1, pp.93-125, 1997.
DOI : 10.1016/S0304-3975(96)00171-5

J. Ketema and J. G. Simonsen, Infinitary Combinatory Reduction Systems, Information and Computation, vol.209, issue.6, pp.893-926, 2011.
DOI : 10.1016/j.ic.2011.01.007

Y. Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004.
DOI : 10.1016/j.tcs.2003.10.018

X. Leroy and H. Grall, Coinductive big-step operational semantics, Information and Computation, vol.207, issue.2, pp.284-304, 2009.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

J. Maraist, M. Odersky, D. N. Turner, and P. Wadler, 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

D. Mazza, An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.471-480, 2012.
DOI : 10.1109/LICS.2012.57

M. Parigot, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, LPAR, pp.190-201, 1992.

M. Parigot, Recursive programming with proofs, Theoretical Computer Science, vol.94, issue.2, pp.335-336, 1992.
DOI : 10.1016/0304-3975(92)90042-E

C. Raffalli, Data types, infinity and equality in system AF 2, CSL, pp.280-294, 1993.
DOI : 10.1007/BFb0049337

A. K. Simpson, Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics, RTA, pp.219-234, 2005.
DOI : 10.1007/978-3-540-32033-3_17

K. Terui, Computational ludics, Theoretical Computer Science, vol.412, issue.20, pp.2048-2071, 2011.
DOI : 10.1016/j.tcs.2010.12.026

C. Wadsworth, Some unusual ?-calculus numeral systems, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

K. Weihrauch, Computable analysis: an introduction, 2000.