Sep 28, 2015
Steven Ramsay: Deciding contextual equivalence for IMJ*
I will describe joint work with Andrzej Murawski and Nikos Tzevelekos in which we consider the problem of deciding observational equivalence for IMJ*.? IMJ* is a kind of maximal fragment of the language Interface Middleweight Java (IMJ)?for which the problem is decidable. Given two, possibly open (containing free identi?ers), terms of IMJ*, the contextual equivalence problem asks if the terms can be distinguished by any possible IMJ context.? Our decision procedure reduces this problem to the emptiness problem for fresh-register pushdown automata.? I will demonstrate our implementation of the procedure in?the tool Coneqct.