DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2024.57

Higher-Order Constrained Dependency Pairs for (Universal) Computability

Authors: Liye Guo, Kasper Hagens, Cynthia Kop, and Deivid Vale

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract

Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs.

Cite as

Liye Guo, Kasper Hagens, Cynthia Kop, and Deivid Vale. Higher-Order Constrained Dependency Pairs for (Universal) Computability. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guo_et_al:LIPIcs.MFCS.2024.57,
  author =	{Guo, Liye and Hagens, Kasper and Kop, Cynthia and Vale, Deivid},
  title =	{{Higher-Order Constrained Dependency Pairs for (Universal) Computability}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{57:1--57:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.57},
  URN =		{urn:nbn:de:0030-drops-206137},
  doi =		{10.4230/LIPIcs.MFCS.2024.57},
  annote =	{Keywords: Higher-order term rewriting, constrained rewriting, dependency pairs}
}

Search Results

Documents authored by Hagens, Kasper

Higher-Order Constrained Dependency Pairs for (Universal) Computability

Abstract

Cite as

Thanks for your feedback!

Could not send message