Higher-Order LCTRSs and Their Termination
Logic in Computer Science
2023-07-26 v1
Abstract
Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of imperative programs so far. In this paper, we present a higher-order variant of the LCTRS formalism, which can be used to analyze functional programs. Then we study the termination problem and define a higher-order recursive path ordering (HORPO) for this new formalism.
Cite
@article{arxiv.2307.13519,
title = {Higher-Order LCTRSs and Their Termination},
author = {Liye Guo and Cynthia Kop},
journal= {arXiv preprint arXiv:2307.13519},
year = {2023}
}
Comments
Presented at WST 2023