Abstract
We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is unit → unit → unit. At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., Ghica, D., Murawski, A.S., Ong, C.-H.L., Stark, I.: Nominal games and full abstraction for the nu-calculus. In: LICS, pp. 150–159 (2004)
Abramsky, S., McCusker, G.: Call-by-Value Games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL, pp. 340–353 (2009)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC, pp. 202–211 (2004)
Benton, N., Leperchey, B.: Relational Reasoning in a Nominal Semantics for Storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 86–101. Springer, Heidelberg (2005)
Cheng, E.Y.C., Kaminski, M.: Context-free languages over infinite alphabets. Acta Inf. 35(3), 245–267 (1998)
Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: ICFP, pp. 143–156 (2010)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13, 341–363 (2002)
Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. TCS 221(1-2), 393–456 (1999)
Hopkins, D., Murawski, A.S., Ong, C.-H.L.: A Fragment of ML Decidable by Visibly Pushdown Automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 149–161. Springer, Heidelberg (2011)
Jeffrey, A., Rathke, J.: Towards a theory of bisimulation for local names. In: LICS (1999)
Kozen, D.: Automata and Computability. Springer (1997)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: POPL, pp. 141–152 (2006)
Laird, J.: A game semantics of names and pointers. APAL 151, 151–169 (2008)
Murawski, A.S.: Functions with local state: regularity and undecidability. TCS 338 (2005)
Murawski, A.S., Tzevelekos, N.: Full Abstraction for Reduced ML. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 32–47. Springer, Heidelberg (2009)
Murawski, A.S., Tzevelekos, N.: Algorithmic Nominal Game Semantics. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 419–438. Springer, Heidelberg (2011)
Murawski, A.S., Tzevelekos, N.: Game semantics for good general references. In: LICS (2011)
Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, Pitts (eds.) Higher-Order Operational Techniques in Semantics, pp. 227–273. CUP (1998)
Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Sci. Comput. Program. 50(1-3), 129–160 (2004)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1), 5:1–5:69 (2011)
Tzevelekos, N.: Full abstraction for nominal general references. LMCS 5(3:8) (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murawski, A.S., Tzevelekos, N. (2012). Algorithmic Games for Full Ground References. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-31585-5_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31584-8
Online ISBN: 978-3-642-31585-5
eBook Packages: Computer ScienceComputer Science (R0)