2026-07-21T21:08:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23635 2025-10-27T10:30:27Z ddc:004 open_access

An Innermost DP Framework for Constrained Higher-Order Rewriting Fuhs, Carsten Guo, Liye Kop, Cynthia Higher-order term rewriting constrained rewriting innermost termination call by value open-world analysis dependency pairs Logically constrained simply-typed term rewriting systems (LCSTRSs) are a higher-order formalism for program analysis with support for primitive data types. The termination problem of LCSTRSs has been studied so far in the setting of full rewriting. This paper modifies the higher-order constrained dependency pair framework to prove innermost termination, which corresponds to the termination of programs under call by value. We also show that the notion of universal computability with respect to innermost rewriting can be effectively handled in the modified, innermost framework, which lays the foundation for open-world termination analysis of programs under call by value via LCSTRSs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Carsten Fuhs and Liye Guo and Cynthia Kop 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.20 urn:nbn:de:0030-drops-236359 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.20 eng https://creativecommons.org/licenses/by/4.0/legalcode