Game Semantic Analysis of Equivalence in IMJ

Abstract. Using game semantics, we investigate the problem of verifying contextual equivalences in Interface Middleweight Java (IMJ), an imperative object calculus in which program phrases are typed using interfaces. Working in the setting where data types are non-recursive and restricted to finite domains, we identify the frontier between decidability and undecidability by reference to the structure of interfaces present in typing judgments. In particular, we show how to determine the decidability status of problem instances (over a fixed type signature) by examining the position of methods inside the term type and the types of its free identifiers. Our results build upon the recent fully abstract game semantics of IMJ. Decidability is proved by translation into visibly pushdown register automata over infinite alphabets with fresh-input recognition.

• Type: Journal
• Year: 2015
• Where: ATVA
• Authors: Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
• Keywords: ATVA 2015, Hardware