Deciding Contextual Equivalence of $$\nu $$ -Calculus with Effectful Contexts

We prove decidability for contextual equivalence of the $$\lambda \mu \nu $$ -calculus, that is the simply-typed call-by-value $$\lambda \mu $$ -calculus equipped with booleans and fresh name creation, with contexts taken in $$\lambda \mu _{\texttt{ref}}$$ , that is $$\lambda \mu \nu $$ -calculus extended with higher-order references. The proof exploits a labelled transition system capturing the interactions between $$\lambda \mu \nu $$ programs and $$\lambda \mu _{\texttt{ref}}$$ contexts. The induced bisimulation equivalence is characterized as equality of certain trees, inspired by the work of Lassen. Since these trees are computable and finite, decidability follows. Bisimulation coincides also with trace equivalence, which in turn coincides with contextual equivalence.