Report
Higher-Order LCTRSs and Their Termination
| العنوان: | Higher-Order LCTRSs and Their Termination |
|---|---|
| المؤلفون: | Guo, Liye, Kop, Cynthia |
| سنة النشر: | 2023 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
| الوصف: | 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. Comment: Presented at WST 2023 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2307.13519 |
| رقم الانضمام: | edsarx.2307.13519 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |