ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States

We prove that the observational equivalence problem for a finitary fragment of the programming langauge ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). This result has two natural and independent parts. We first prove that the observational equivalence problem is equivalent to the emptiness problem for a new class of class memory automata equipped with a visibly pushdown stack, called Visibly Pushdown Class Memory Automata (VPCMA). Our proof uses the fully abstract game semantics of the language. We then prove that the VPCMA emptiness problem is equivalent to the reachability problem for EBVASS. The results of this article complete our programme to give an automata classification of the ML types with respect to the observational equivalence problem for closed terms.