Algorithmic games for full ground references.
Journal:
Formal methods in system design
Published Date:
Aug 9, 2017
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 . 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
Keywords
No keywords available for this article.