DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.12

Unbounded Data Nesting for Loops in Higher-Order Programs

Authors: Adriana Baldacchino and Andrzej S. Murawski

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

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.

Cite as

Adriana Baldacchino and Andrzej S. Murawski. Unbounded Data Nesting for Loops in Higher-Order Programs. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{baldacchino_et_al:LIPIcs.LICS.2026.12,
  author =	{Baldacchino, Adriana and Murawski, Andrzej S.},
  title =	{{Unbounded Data Nesting for Loops in Higher-Order Programs}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{12:1--12:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.12},
  URN =		{urn:nbn:de:0030-drops-267990},
  doi =		{10.4230/LIPIcs.LICS.2026.12},
  annote =	{Keywords: Automata theory, automata over infinite alphabets, programming language semantics, contextual equivalence, game semantics}
}

Search Results

Documents authored by Baldacchino, Adriana

Unbounded Data Nesting for Loops in Higher-Order Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message