The monadic second order theory of trees given by arbitrary leveltwo recursion schemes is decidable, TLCA'05, pp.39-54, 2005. ,
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. ,
The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984. ,
A saturation method for collapsible pushdown systems, In ICALP LNCS, vol.7392, issue.2, pp.165-176, 2012. ,
Logical theories and compatible operations, Logic and Automata Logic and Games, pp.73-106, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00199044
An extension to Muchnik's theorem, Journal of Logic and Computation, vol.13, pp.59-74, 2005. ,
On infinite terms having a decidable monadic theory, MFCS'02, pp.165-176, 2002. ,
DOI : 10.1007/3-540-45687-2_13
The evaluation of firstorder substitution is monadic second-order compatible, TCS, vol.281, pp.177-206, 2002. ,
The evaluation of firstorder substitution is monadic second-order compatible, TCS, vol.281, issue.12, pp.177-206, 2002. ,
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
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
The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata, FSTTCS'03, pp.112-124, 2003. ,
The IO-and OI-hierarchies, Theor. Comp. Sci, vol.20, pp.95-207, 1982. ,
Grammars with macro-like productions, 1968. ,
The first order properties of products of algebraic systems, Fundamenta Mathematicae, vol.47, pp.57-103, 1959. ,
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
Term Rewriting Systems , volume 55 of Cambridge Tracts in Theoretical Computer Science, chapter 12, pp.668-711, 2003. ,
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
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
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
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
A type system equivalent to modal mu-calculus model checking of recursion schemes, LICS, pp.179-188, 2009. ,
Complexity of model checking recursion schemes for fragments of the modal mucalculus, Logical Methods in Computer Science, vol.7, issue.4, 2011. ,
Higher-order program verification and languagebased security, ASIAN, pp.17-23, 2009. ,
Types and higher-order recursion schemes for verification of higher-order programs, POPL, pp.416-428, 2009. ,
Types and recursion schemes for higher-order program verification, APLAS, pp.2-3, 2009. ,
A call-by-name lambda-calculus machine. Higher- Order and Symbolic Computation, pp.199-207, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00154508
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. ,
On model-checking trees generated by higherorder recursion schemes, LICS, pp.81-90, 2006. ,
Verifying higherorder functional programs with pattern-matching algebraic data types, POPL, pp.587-598, 2011. ,
On the significance of the collapse operation, LICS, pp.521-530, 2012. ,
LCF considered as a programming language, Theor. Comput. Sci, vol.5, issue.3, pp.223-255, 1977. ,
Decidability of second-order theories and automata on infinite trees, Transactions of the AMS, vol.141, pp.1-23, 1969. ,
Recognizability in the simply typed lambdacalculus, WoLLIC, pp.48-60, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00412654
Decidability of monadic theories, MFCS'84, pp.162-175, 1984. ,
The monadic second order theory of order, Annals of Mathematics, vol.102, pp.379-419, 1975. ,
On the ?y calculus, Annals of Pure and Applied Logic, vol.130, issue.1-3, pp.325-337, 2004. ,
The lattice-model is recursive in the original model, 1975. ,
Krivine machines and higherorder schemes, ICALP, pp.162-173, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01121744
Recursive schemes, Krivine machines , and collapsible pushdown automata, RP, pp.6-20, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00717718
Evaluation is MSOL compatible ,
URL : https://hal.archives-ouvertes.fr/hal-00773126
Monadic second-order logic on tree-like structures, Theor. Comput. Sci, vol.275, issue.12, pp.311-346, 2002. ,
Monadic second order logic on tree-like structures, Theoretical Computer Science, vol.257, issue.12, pp.311-346, 2002. ,