Talk "Algorithmic games for full ground references"

by Andrzej Murawski

Sat, 16 March 2013 at 02:00 pm in Rome, Italy

Joint work with: Nikos Tzevelekos (Queen Mary, University of London)

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.