K. Aehlig, J. G. De-miranda, and C. L. Ong, Safety Is not a Restriction at Level 2 for String Languages, FOSSACS, pp.490-504, 2005.
DOI : 10.1007/978-3-540-31982-5_31

A. V. Aho, Indexed Grammars---An Extension of Context-Free Grammars, Journal of the ACM, vol.15, issue.4, pp.647-671, 1968.
DOI : 10.1145/321479.321488

R. M. Amadio and P. Curien, Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00070008

W. Blum and C. L. Ong, The safe lambda calculus, Logical Methods in Computer Science, vol.5, issue.13, pp.1-38, 2009.

P. Bourreau and S. Salvati, A Datalog Recognizer for Almost Affine ??-CFGs, MOL 12, pp.21-38, 2011.
DOI : 10.1007/s10849-009-9110-0
URL : https://hal.archives-ouvertes.fr/hal-00740701

H. Christopher and . Broadbent, The limits of decidability for first order logic on cpda graphs, STACS, pp.589-600, 2012.

W. Damm, The IO- and OI-hierarchies, Theoretical Computer Science, vol.20, issue.2, pp.95-207, 1982.
DOI : 10.1016/0304-3975(82)90009-3

P. De-groote, Towards abstract categorial grammars, Proceedings of the 39th Annual Meeting on Association for Computational Linguistics , ACL '01, pp.148-155, 2001.
DOI : 10.3115/1073012.1073045
URL : https://hal.archives-ouvertes.fr/inria-00100529

P. De-groote and E. Lebedeva, On the dynamics of proper names, 2010.

P. De-groote and E. Lebedeva, Presupposition accommodation as exception handling, SIGDIAL, pp.71-74, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00572852

J. Engelfriet, Iterated stack automata and complexity classes, Information and Computation, vol.95, issue.1, pp.21-75, 1991.
DOI : 10.1016/0890-5401(91)90015-T

M. J. Fischer, Grammars with macro-like productions, 9th Annual Symposium on Switching and Automata Theory (swat 1968), 1968.
DOI : 10.1109/SWAT.1968.12

A. Haddad, IO vs OI in Higher-Order Recursion Schemes, FICS, pp.23-30, 2012.
DOI : 10.4204/EPTCS.77.4
URL : https://hal.archives-ouvertes.fr/hal-00865681

G. Huet, Résolution d'´ equations dans des langages d'ordre 1, Thèse de doctorat en sciences mathématiques, 1976.

M. Kanazawa, Parsing and generation as datalog queries, Proceedings of the 45th Annual Meeting of ACL, pp.176-183, 2007.

T. Knapik, D. Niwinski, and P. Urzyczyn, Higher-Order Pushdown Trees Are Easy, FoSSaCS, volume 2303 of LNCS, pp.205-222, 2002.
DOI : 10.1007/3-540-45931-6_15

E. Lebedeva, Expressing Discourse Dynamics Through Continuations, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00783245

R. Loader, The undecidability of ?-definability. In Logic, Meaning and Computation: Essays in memory of Alonzo Church, pp.331-342, 2001.

R. Montague, Formal Philosophy: Selected Papers of Richard Montague, 1974.

Y. Moschovakis, Sense and denotation as algorithm and value. In Logic Collo- quium'90: ASL Summer Meeting in Helsinki, p.210, 1993.
DOI : 10.1017/9781316718254.015
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.433.3881

R. Muskens, Lambda Grammars and the Syntax-Semantics Interface, Proceedings of the Thirteenth Amsterdam Colloquium, pp.150-155, 2001.

C. L. Ong, On Model-Checking Trees Generated by Higher-Order Recursion Schemes, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pp.81-90, 2006.
DOI : 10.1109/LICS.2006.38

P. Parys, On the Significance of the Collapse Operation, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.521-530, 2012.
DOI : 10.1109/LICS.2012.62

S. Salvati, Recognizability in the Simply Typed Lambda-Calculus, 16th WOL- LIC, pp.48-60, 2009.
DOI : 10.1016/0095-8956(86)90030-4
URL : https://hal.archives-ouvertes.fr/inria-00412654

S. Salvati, On the Membership Problem for Non-Linear Abstract Categorial Grammars, Journal of Logic, Language and Information, vol.10, issue.1, pp.163-183, 2010.
DOI : 10.1007/s10849-009-9110-0
URL : https://hal.archives-ouvertes.fr/hal-00306230

S. Salvati, G. Manzonetto, M. Gehrke, and H. Barendregt, Loader and Urzyczyn Are Logically Related, ICALP (2), pp.364-376, 2012.
DOI : 10.1007/978-3-642-31585-5_34
URL : https://hal.archives-ouvertes.fr/hal-00959623

S. Salvati and I. Walukiewicz, Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata, RP, pp.6-20, 2012.
DOI : 10.1007/978-3-642-33512-9_2
URL : https://hal.archives-ouvertes.fr/hal-00717718

R. Statman, Completeness, invariance and ??-definability, The Journal of Symbolic Logic, vol.344, issue.01, pp.17-26, 1982.
DOI : 10.1016/0304-3975(76)90021-9

K. Terui, Semantic evaluation, intersection types and complexity of simply typed lambda calculus, RTA, pp.323-338, 2012.

I. Van-rooij, The Tractable Cognition Thesis, Cognitive Science: A Multidisciplinary Journal, vol.32, issue.6, pp.939-984, 2008.
DOI : 10.1080/03640210801897856

E. (. A1, B (f )) is in I A2,B,? 2. if ? = ? ? ? and g is in M ? (B) then (? A2,? , E A1,B (f )(g)) is in I A2

?. A2, = ? and since f ? A 1 and A 1 is disjoint from A 2 we have that f ? A 2 = ?. It thus follows that (?, f ) is well in I A2,B,? . In case ? = ? ? ?, let (h, l) be in I A2,B,? , we need to show that (? A2,? , E A1,B (f )(l)) is in I A2,B,? . We have that (k) ? l}. As, by induction, we have that, (f (k))) is in I A2,B,? and that, by the previous Lemma (? A2,? , ? B,? ) is in I A2,B,? , we obtain, using iteratively Lemma 4, that (? A2,? , E A1,B (f )(l)) is in I A2

. Lemma-8, Given a type ? we have the following properties: 1. for every f in M ? (A), (f, E A,B (f )) is in I A,B,? , 2. for every (f, g) in I A,B,? , for every h in M ? (A)

. Proof, We proceed by induction on the structure of ?. The case where ? = 0 is clear

I. A. In, (l)) | E A,B (l) ? g 2 }. But by induction hypothesis (l) ? g 2 iff l ? g 1 (l)) | l ? g 1 }. But the induction hypothesis also implies that (f (g 1 ), E A,B (f (g 1 ))) is in I A,B,? , and by monotonicity of f , if l ? g 1 , then f (l) ? f (g 1 ), which by induction is equivalent to, Therefore {E A,B (f (l)) | l ? g 1 } = E A,B (f (g 1 )), E A,B (f )(g 2 ) =