Contextual Equivalence for State and Control via Nested Data
Benedict Bunting, Andrzej S. Murawski · 2024
We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is decidable for all programs with first-order references and continuations, assuming they have continuation- and reference-free interfaces. This is the best one can hope for in this case, because the addition of references to functions, to continuations or to references makes the problem undecidable.