Sciweavers

ATVA
2015
Springer

Game Semantic Analysis of Equivalence in IMJ

7 years 11 months ago
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.
Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzeve
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where ATVA
Authors Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
Comments (0)