C. Broadbent and C. Ong, On Global Model Checking Trees Generated by Higher-Order Recursion Schemes, Proceedings of 12th International Conference on Foundations of Software Science and Computational Structures, pp.107-121, 2009.
DOI : 10.1016/S0020-0190(02)00445-3

C. Carayol, M. Hague, A. Meyer, L. Ong, and O. Serre, Winning Regions of Higher-Order Pushdown Games, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.193-204, 1958.
DOI : 10.1109/LICS.2008.41
URL : https://hal.archives-ouvertes.fr/hal-00345939

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

W. Damm and E. Fehr, A schematalogical approach to the alalysis of the procedure concept in algol-languages, CLAAP, pp.130-134, 1980.

H. , M. Hague, A. S. Murawski, C. Ong, and O. 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

A. Kartzow, Collapsible pushdown graphs of level 2 are treeautomatic Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, STACS, volume 5 of LIPIcs KNU02. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy Proc. FoSSaCS'02, pp.501-512, 2002.

T. Knapik, D. Niwinski, P. Urzycyzn, and I. Walukiewicz, Unsafe grammars and pannic automata A type system equivalent to modal mucalculus model checking of recursion schemes, ICALP 05, number 3580 in LNCS Proceedings of 24th Annual IEEE Symposium on Logic in Computer Science, pp.1450-1461, 2005.

K. Krivine, A call-by-name lambda-calculus machine. Higher- Order and Symbolic Computation On model-checking trees generated by higher-order recursion schemes, LICS, pp.199-207, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00154508

G. D. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5

W. and I. Walukiewicz, Pushdown Processes: Games and Model Checking, BRICS Report Series, vol.3, issue.54, pp.234-263, 2001.
DOI : 10.7146/brics.v3i54.20057
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4162

W. and M. Wand, On the correctness of the krivine machine. Higher-Order and Symbolic Computation, pp.231-235, 2007.

. Since-q-ix-i,-?-i, S i ) is winning we get that (q i , r ) ? ? i (x i )(S i ) for some r . Moreover, as x i is a variable free in N , we either have ? i (x i ) = ? N (x i ) (when N is of the form x i N 1 . . . N p ) or ? i (x i ) = ? N (x i ) r for some r

. So, there is r i such that (q i , r i ) ? ? N (x i )(S i ) But then, as we have noted above, Eve has a winning strategy from q : (term(t i ), ?, S i ) is