K. Aehlig, J. G. De-miranda, and C. Ong, The monadic second order theory of trees given by arbitrary leveltwo recursion schemes is decidable, TLCA'05, pp.39-54, 2005.

K. Aehlig, A finite semantics of simply-typed lambda terms for infinite runs of automata, Logical Methods in Computer Science, vol.3, issue.1, pp.1-23, 2007.

]. H. Bar84 and . Barendregt, The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984.

H. Christopher, A. Broadbent, M. Carayol, O. Hague, and . Serre, A saturation method for collapsible pushdown systems, In ICALP LNCS, vol.7392, issue.2, pp.165-176, 2012.

[. Blumensath, T. Colcombet, and C. Löding, Logical theories and compatible operations, Logic and Automata Logic and Games, pp.73-106, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00199044

A. Blumensath and S. Kreutzer, An extension to Muchnik's theorem, Journal of Logic and Computation, vol.13, pp.59-74, 2005.

D. Caucal, On infinite terms having a decidable monadic theory, MFCS'02, pp.165-176, 2002.
DOI : 10.1007/3-540-45687-2_13

[. Courcelle and T. Knapik, The evaluation of firstorder substitution is monadic second-order compatible, TCS, vol.281, pp.177-206, 2002.

[. Courcelle and T. Knapik, The evaluation of firstorder substitution is monadic second-order compatible, TCS, vol.281, issue.12, pp.177-206, 2002.

[. Courcelle, Monadic second-order graph transductions: A survey, Theoretical Computer Science, vol.126, pp.53-75, 1994.
DOI : 10.1016/0304-3975(94)90268-2

URL : http://doi.org/10.1016/0304-3975(94)90268-2

[. Courcelle and I. Walukiewicz, Monadic second-order logic, graphs and unfoldings of transition systems, Ann. of Pure and Appl. Log, vol.92, pp.35-62, 1998.
DOI : 10.7146/brics.v2i44.19945

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.2520

S. [. Carayol and . Wöhrle, The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata, FSTTCS'03, pp.112-124, 2003.

]. W. Dam82 and . Damm, The IO-and OI-hierarchies, Theor. Comp. Sci, vol.20, pp.95-207, 1982.

]. M. Fis68 and . Fischer, Grammars with macro-like productions, 1968.

R. [. Feferman and . Vaught, The first order properties of products of algebraic systems, Fundamenta Mathematicae, vol.47, pp.57-103, 1959.

A. [. Hague, C. L. Murawski, O. Ong, and . Serre, Collapsible pushdown automata and recursion schemes, LICS, pp.452-461, 2008.
DOI : 10.1109/lics.2008.34

URL : https://hal.archives-ouvertes.fr/hal-00345945

R. Kennaway and F. Vries, Term Rewriting Systems , volume 55 of Cambridge Tracts in Theoretical Computer Science, chapter 12, pp.668-711, 2003.

[. Kennaway, J. W. Klop, M. R. Sleep, and F. Vries, Infinitary lambda calculus, Theor. Comput. Sci, vol.175, issue.1, pp.93-125, 1997.
DOI : 10.1016/s0304-3975(96)00171-5

URL : http://doi.org/10.1016/s0304-3975(96)00171-5

D. Kuske and M. Lohrey, Monadic chain logic over iterations and applications to pushdown systems, LICS, pp.91-100, 2006.
DOI : 10.1109/lics.2006.35

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.4915

D. [. Knapik, P. Niwinski, and . Urzyczyn, Higher-order pushdown trees are easy, FoSSaCS, pp.205-222, 2002.
DOI : 10.1007/3-540-45931-6_15

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.5773

D. [. Knapik, P. Niwinski, I. Urzycyzn, and . Walukiewicz, Unsafe grammars and pannic automata, ICALP, pp.1450-1461, 2005.
DOI : 10.1007/11523468_117

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.484.3216

L. [. Kobayashi and . Ong, A type system equivalent to modal mu-calculus model checking of recursion schemes, LICS, pp.179-188, 2009.

[. Kobayashi and C. Ong, Complexity of model checking recursion schemes for fragments of the modal mucalculus, Logical Methods in Computer Science, vol.7, issue.4, 2011.

]. N. Kob09a and . Kobayashi, Higher-order program verification and languagebased security, ASIAN, pp.17-23, 2009.

]. N. Kob09b and . Kobayashi, Types and higher-order recursion schemes for verification of higher-order programs, POPL, pp.416-428, 2009.

]. N. Kob09c and . Kobayashi, Types and recursion schemes for higher-order program verification, APLAS, pp.2-3, 2009.

[. Krivine, A call-by-name lambda-calculus machine. Higher- Order and Symbolic Computation, pp.199-207, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00154508

[. Kuske, Compatibility of Shelah and Stupp's and Muchnik's iteration with fragments of monadic second order logic, STACS, volume 1 of LIPIcs, pp.467-478, 2008.

]. L. Ong06 and . Ong, On model-checking trees generated by higherorder recursion schemes, LICS, pp.81-90, 2006.

[. Ong, S. J. , and R. , Verifying higherorder functional programs with pattern-matching algebraic data types, POPL, pp.587-598, 2011.

P. Parys, On the significance of the collapse operation, LICS, pp.521-530, 2012.

]. G. Plo77 and . Plotkin, LCF considered as a programming language, Theor. Comput. Sci, vol.5, issue.3, pp.223-255, 1977.

]. M. Rab69 and . Rabin, Decidability of second-order theories and automata on infinite trees, Transactions of the AMS, vol.141, pp.1-23, 1969.

[. Salvati, Recognizability in the simply typed lambdacalculus, WoLLIC, pp.48-60, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00412654

]. A. Sem84 and . Semenov, Decidability of monadic theories, MFCS'84, pp.162-175, 1984.

[. Shelah, The monadic second order theory of order, Annals of Mathematics, vol.102, pp.379-419, 1975.

[. Statman, On the ?y calculus, Annals of Pure and Applied Logic, vol.130, issue.1-3, pp.325-337, 2004.

J. Stupp, The lattice-model is recursive in the original model, 1975.

I. [. Salvati and . Walukiewicz, Krivine machines and higherorder schemes, ICALP, pp.162-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01121744

I. [. Salvati and . Walukiewicz, Recursive schemes, Krivine machines , and collapsible pushdown automata, RP, pp.6-20, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00717718

I. [. Salvati and . Walukiewicz, Evaluation is MSOL compatible
URL : https://hal.archives-ouvertes.fr/hal-00773126

I. Walukiewicz, Monadic second-order logic on tree-like structures, Theor. Comput. Sci, vol.275, issue.12, pp.311-346, 2002.

I. Walukiewicz, Monadic second order logic on tree-like structures, Theoretical Computer Science, vol.257, issue.12, pp.311-346, 2002.