Abstract
We survey recent developments in an approach to the verification of higher-order computation based on game semantics. Higher-order recursion schemes are in essence (programs of) the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. They are a highly expressive definitional device for infinite structures such as word languages and infinite ranked trees. As applications of a representation theory of innocent strategies based on traversals, we present a recent advance in the model checking of trees generated by recursion schemes, and the first machine characterization of recursion schemes (by a new variant class of higher-order pushdown automata called collapsible pushdown automata). We conclude with some speculative remarks about reachability checking of functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and verification.
Chapter PDF
References
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135–150 (1997)
Abramsky, S., Honda, K., McCusker, G.: Fully abstract game semantics for general reference. In: Proceedings of IEEE Symposium on Logic in Computer Science, 1998, Computer Society Press (1998)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163 (2000)
Abramsky, S., McCusker, G.: Linearity, sharing and state: A fully abstract game semantics for Idealized Algol with active expressions. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-like languages, Birkhäuser (1997)
Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, Springer, Heidelberg (1998)
Abramsky, S., McCusker, G.: Game semantics. In: Schwichtenberg, H., Berger, U. (eds.) Logic and Computation: Proceedings of the 1997 Marktoberdorf Summer School, Springer, Heidelberg (1998)
Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: The monadic second order theory of trees given by arbitrary level two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)
Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: Safety is not a restriction at level 2 for string languages. In: Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2005). LNCS, vol. 3411, pp. 490–501. Springer, Heidelberg (2005)
Ball, T., Rajamani, S.K.: The SLAM Project: Debugging system software via static analysis. In: Proc. POPL, pp. 1–3. ACM Press, New York (2002)
Blum, W.: The Safe Lambda Calculus. PhD thesis, University of Oxford (in preparation, 2008)
Blum, W., Ong, C.-H.L.: Safe lambda calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 39–53. Springer, Heidelberg (2007)
Blum, W., Ong, C.-H.L.: Path-correspondence theorems and their applications (preprint, 2008)
Caucal, D.: On Infinite Terms Having a Decidable Monadic Theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 165–176. Springer, Heidelberg (2002)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Damm, W.: The IO- and OI-hierarchy. Theoretical Computer Science 20, 95–207 (1982)
Damm, W., Goerdt, A.: An automata-theoretical characterization of the OI-hierarchy. Information and Control 71, 1–32 (1986)
de Roever, W.-P., de Bakker, J.W.: A calculus for recursive program schemes. In: Nivat, M. (ed.) Proc. IRIA symposium on Automata, Languages and Programming, North-Holland, Amsterdam (1972)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS 1991, pp. 368–377 (1991)
Ghica, D.R., McCusker, G.: Reasoning about Idealized ALGOL Using Regular Languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 103–116. Springer, Heidelberg (2000)
Greenland, W.: Game semantics for region analysis. PhD thesis, Oxford University Computing Laboratory (2005)
Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. Technical report, Oxford University Computing Laboratory, p. 59 (preprint, 2007), http://users.comlab.ox.ac.uk/luke.ong/
Hankin, C., Malacaria, P.: A new approach to control flow analysis. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 95–108. Springer, Heidelberg (1998)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Proc. 10th SPIN Workshop (2003)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation (extended abstract). In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, Springer, Heidelberg (1997)
Hyland, J.M.E., Ong, C.-H.L.: On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation 163, 285–408 (2000)
Walukiewicz, I.: Model Checking CTL Properties of Pushdown Systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, Springer, Heidelberg (2000)
Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-Order Pushdown Trees Are Easy. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)
Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I.: Unsafe Grammars and Panic Automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1450–1461. Springer, Heidelberg (2005)
Laird, J.: A semantic analysis of control. PhD thesis, University of Edinburgh (1998)
Maslov, A.N.: Multilevel stack automata. Problems of Information Transmission 12, 38–43 (1976)
Might, M., Chambers, B., Shivers, O.: Model Checking Via ΓCFA. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 59–73. Springer, Heidelberg (2007)
Murawski, A., Walukiewicz, I.: Third-Order Idealized Algol with Iteration Is Decidable. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 202–218. Springer, Heidelberg (2005)
Murawski, A.S., Ong, C.-H.L., Walukiewicz, I.: Idealized Algol with ground recursion and DPDA equivalence. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 917–929. Springer, Heidelberg (2005)
Nivat, M.: On the interpretation of recursive polyadic program schemes. Symp. Math. XV, 255–281 (1975)
Ong, C.-H.L.: Observational equivalence of third-order Idealized Algol is decidable. In: Proceedings of IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 22-25, 2002, pp. 245–256. Computer Society Press (2002)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings 21st Annual IEEE Symposium on Logic in Computer Science, Seattle, pp. 81–90. Computer Society Press (2006), users.comlab.ox.ac.uk/luke.ong/
Padovani, V.: Decidability of all minimal models. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 201–215. Springer, Heidelberg (1996)
Padovani, V.: Decidability of fourth-order matching. Math. Struct. in Comp. Science 10, 361–372 (2000)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Maths. Soc. 141, 1–35 (1969)
Schubert, A.: A linear interpolation for the higher-order matching problem. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 441–452. Springer, Heidelberg (1997)
Shivers, O.: Control-flow analysis of higher-order languages. PhD thesis, Carnegie-Mellon University (1991)
Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. IEEE Annual Symposium on Logic in Computer Science, IEEE Computer Society Press (1986)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ong, C.H.L. (2008). Verification of Higher-Order Computation: A Game-Semantic Approach. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)