ML and Extended Branching VASS

We prove that the observational equivalence problem for a finitary fragment of ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). Our proof uses the fully abstract game semantics of the language. We introduce a new class of a...

Full description

Bibliographic Details
Main Authors: Cotton-Barratt, C, Ong, C, Murawski, A
Format: Conference item
Published: Springer 2017