Algorithmic games for full ground references

Journal article

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.

Authors: Murawski, AS; Tzevelekos, N

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Journal: Formal Methods in System Design
• Volume: 52
• Issue: 3
• Pages: 277-314
• Publication date: 2017-08-09
• DOI: 10.1007/s10703-017-0292-9
• EISSN: 1572-8102
• ISSN: 0925-9856
• Language: English
• Keywords: Semantics (computer science); Discrete mathematics; Programming language; Theoretical computer science; Decidability; Computer science; Game semantics; Mathematics; Unit (ring theory); Automaton; Finitary; Undecidable problem; Equivalence (formal languages); Operational semantics