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. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Murawski, A. S., & Tzevelekos, N. (2012). Algorithmic games for full ground references. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7392 LNCS, pp. 312–324). Springer Verlag. https://doi.org/10.1007/978-3-642-31585-5_30
Mendeley helps you to discover research relevant for your work.