POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 15:30 - 15:50 at Turing Lecture - Algorithmic Verification Chair(s): Andreas Pavlogiannis

We consider first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic.

We also give a calculus, based on prime functions and combinators, which derives all first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, co-products and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus.

As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also to MSO interpretations.

Thu 18 Jan

Displayed time zone: London change

15:30 - 16:50
Algorithmic VerificationPOPL at Turing Lecture
Chair(s): Andreas Pavlogiannis Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk Warsaw University, Bartek Klin University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
Pre-print