L. T. Nguy?ênnguy?-nguy?ên and P. Pradic, From normal functors to subpolynomial queries, 2019.

J. Girard, The system F of variable types, fifteen years later, Theoretical Computer Science, vol.45, pp.159-192, 1986.

, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-101, 1987.

K. Terui, Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus, RTA'12, 2012.

I. Walukiewicz and S. Salvati, Using models to model-check recursive schemes, Logical Methods in Computer Science, vol.11, issue.2, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00741077

, Typing weak MSOL properties, Logical Methods in Computer Science, vol.13, issue.1, 2017.

K. Aehlig, A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata, Logical Methods in Computer Science, vol.3, issue.3, 2007.

M. Hofmann and J. Ledent, A cartesian-closed category for higherorder model checking, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017.

G. G. Hillebrand and P. C. Kanellakis, On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi, LICS'96, 1996.

C. Grellois and P. Melliès, Relational Semantics of Linear Logic and Higher-order Model Checking, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), ser. Leibniz International Proceedings in Informatics (LIPIcs), S. Kreutzer, vol.41, pp.260-276, 2015.

C. Grellois, Semantics of linear logic and higher-order modelchecking, 2016.
URL : https://hal.archives-ouvertes.fr/tel-01311150

D. Baelde, Least and Greatest Fixed Points in Linear Logic, ACM Transactions on Computational Logic, vol.13, issue.1, pp.1-44, 2012.

P. Baillot, On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy, Information and Computation, vol.241, pp.3-31, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01948302

G. G. Hillebrand, Finite Model Theory in the Simply Typed Lambda Calculus, 1994.

U. Schöpp, Stratified Bounded Affine Logic for Logarithmic Space, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.411-420, 2007.

U. Lago and U. Schöpp, Computation by interaction for spacebounded functional programming, Information and Computation, vol.248, pp.150-194, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01337724

D. Mazza, Simple Parsimonious Types and Logarithmic Space, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), ser. Leibniz International Proceedings in Informatics (LIPIcs), S. Kreutzer, vol.41, pp.24-40, 2015.

J. Girard, Light Linear Logic, Information and Computation, vol.143, issue.2, pp.175-204, 1998.

Q. Ma and J. C. Reynolds, Types, abstraction, and parametric polymorphism, Mathematical foundations of programming semantics, vol.II, pp.1-40, 1991.

E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott, Functorial polymorphism, Theor. Comput. Sci, vol.70, issue.1, pp.90151-90158, 1990.

G. Longo, K. Milsted, and S. Soloviev, The genericity theorem and parametricity in the polymorphic lambda-calculus, Theor. Comput. Sci, vol.121, issue.1-2, pp.90093-90102, 1993.

J. Girard, Quantifiers in linear logic II, pp.79-90, 1991.

L. Tortora-de-falco, Additives of linear logic and normalization-part I: a (restricted) church-rosser property, Theoretical Computer Science, vol.294, pp.489-524, 2003.

M. Pagani and L. Tortora-de-falco, Strong normalization property for second order linear logic, Theoretical Computer Science, vol.441, issue.2, pp.410-444, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00698979

H. G. Mairson and K. Terui, On the Computational Complexity of Cut-Elimination in Linear Logic, Theoretical Computer Science, ser. Lecture Notes in Computer Science, pp.23-36, 2003.

D. J. Hughes and R. J. Van-glabbeek, Proof nets for unit-free multiplicative-additive linear logic, ACM Transactions on Computational Logic (TOCL), vol.6, issue.4, pp.784-842, 2005.

Y. Lafont and A. Scedrov, The Undecidability of Second Order Multiplicative Linear Logic, Information and Computation, vol.125, issue.1, pp.46-51, 1996.

Y. Lafont, The undecidability of second order linear logic without exponentials, The Journal of Symbolic Logic, vol.61, issue.02, pp.541-548, 1996.

V. Danos and J. Joinet, Linear logic and elementary time, Information and Computation, vol.183, issue.1, pp.123-137, 2003.

D. E. Knuth, Mathematics and computer science: Coping with finiteness, Science, vol.194, issue.4271, pp.1235-1242, 1976.

P. Baillot, E. D. Benedetti, and S. Rocca, Characterizing polynomial and exponential complexity classes in elementary lambda-calculus, Information and Computation, vol.261, pp.55-77, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01015171

P. Baillot and A. Ghyselen, Combining Linear Logic and Size Types for Implicit Complexity, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), ser. Leibniz International Proceedings in Informatics (LIPIcs), vol.119, pp.1-9, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01948196

J. Girard, Linear logic: its syntax and semantics, Advances in Linear Logic, ser

Y. Girard, L. Lafont, and . Regnier, , vol.222, 1995.

T. Coquand, Categories of embeddings, Theoretical Computer Science, vol.68, issue.3, pp.221-237, 1989.

N. Gambino and J. Kock, Polynomial functors and polynomial monads, Mathematical Proceedings of the Cambridge Philosophical Society, vol.154, issue.01, pp.153-192, 2013.

A. Bac-bruasse, Logique linéaire indexée du second ordre, 2001.

R. A. Seely, Polymorphic linear logic and topos models, C. R. Math. Rep. Acad. Sci. Canada, vol.12, issue.1, pp.21-26, 1990.

, Categorical semantics for higher order polymorphic lambda calculus, J. Symbolic Logic, vol.52, issue.4, pp.969-989, 1987.

R. Blute, Linear logic, coherence and dinaturality, 4th Summer Conference on Category Theory and Computer Science, vol.115, pp.3-41, 1991.

, , p.90053

P. J. Freyd and J. ,

A. Girard, P. J. Scedrov, and . Scott, Semantic parametricity in polymorphic lambda calculus, Proceedings. Third Annual Symposium on Logic in Computer Science, pp.274-279, 1988.

A. Schalk and H. P. Steele, Constructing fully complete models of multiplicative linear logic, Log. Methods Comput. Sci, vol.11, issue.3, 2015.

R. F. Blute and P. J. Scott, Linear Läuchli semantics, Ann. Pure Appl. Logic, vol.77, issue.2, pp.17-25, 1996.

T. Ehrhard, Parallel and serial hypercoherences, Theoretical Computer Science, vol.247, issue.1, pp.39-81, 2000.
URL : https://hal.archives-ouvertes.fr/hal-00527036

P. Boudes, ;. , D. Hutchison, T. Kanade, J. Kittler et al., Projecting Games on Hypercoherences, Automata, Languages and Programming, vol.3142, pp.257-268, 2004.

P. Melliès, Sequential algorithms and strongly stable functions, Theoretical Computer Science, vol.343, issue.1, pp.237-281, 2005.

S. R. Rocca, On dialogue games and coherent strategies, Computer Science Logic 2013 (CSL 2013), ser. Leibniz International Proceedings in Informatics (LIPIcs), vol.23, pp.540-562, 2013.

J. Laird, Game Semantics for a Polymorphic Programming Language, Journal of the ACM, vol.60, issue.4, pp.1-29, 2013.

G. Jaber and N. Tzevelekos, A Trace Semantics for System F Parametric Polymorphism, Foundations of Software Science and Computation Structures, vol.10803, pp.20-38, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02083207

S. Abramsky, Retracing some paths in process algebra, CONCUR '96: Concurrency Theory, ser. Lecture Notes in Computer Science, pp.1-17, 1996.

K. Terui, Proof nets and boolean circuits, 19th IEEE Symposium on Logic in Computer Science (LICS 2004, pp.182-191, 2004.