Functions with local state: Regularity and undecidability

AbstractWe study programs of a finitary ML-like language RMLf with ground-type references. RMLf permits the use of functions with locally declared variables that remain private and persist from one use of the function to the next. Using game semantics we show that this leads to undecidability of program equivalence already at second order. We also examine the extent to which this feature can be captured by regular languages. This gives a decidability result for a second-order fragment RMLf- of RMLf, which comprises many examples studied in the literature