Unbounded Data Nesting for Loops in Higher-Order Programs

We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems.

Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data.

We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops.

This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.