35 citations · 80 across the 25 of their papers we have counts for
21 papers · 1 filter
Higher-Order Constrained Dependency Pairs for (Universal) Computability
Liye Guo, Kasper Hagens, Cynthia Kop +1
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 framewo…
A weakly monotonic, logically constrained, HORPO-variant
Cynthia Kop
In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for…
A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
Patrick Baillot, Ugo Dal Lago, Cynthia Kop +1
The class of type-two basic feasible functionals () is the analogue of (polynomial time functions) for type-2 functionals, that is, functionals that c…
Higher-Order LCTRSs and Their Termination
Liye Guo, Cynthia Kop
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 f…
Complexity Analysis for Call-by-Value Higher-Order Rewriting
Cynthia Kop, Deivid Vale
In this short paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy so as to model call-by-value programs. We briefly present a cost-size sem…
Certifying Higher-Order Polynomial Interpretations
Niels van der Weide, Deivid Vale, Cynthia Kop
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs,…
Tuple Interpretations and Applications to Higher-Order Runtime Complexity
Cynthia Kop, Deivid Vale
Tuple interpretations are a class of algebraic interpretation that subsumes both polynomial and matrix interpretations as it does not impose simple termination and allows non-linea…
Polymorphic Higher-order Termination
Łukasz Czajka, Cynthia Kop
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we inte…
A static higher-order dependency pair framework
Carsten Fuhs, Cynthia Kop
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism desi…
The unified higher-order dependency pair framework
Carsten Fuhs, Cynthia Kop
In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the d…
On First-order Cons-free Term Rewriting and PTIME
Cynthia Kop
In this paper, we prove that (first-order) cons-free term rewriting with a call-by-value reduction strategy exactly characterises the class of PTIME-computable functions. We use th…
Cons-free Programming with Immutable Functions
Cynthia Kop
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we set out to characterise the hierarchy NP $\subseteq…
Non-deterministic Characterisations
Cynthia Kop
In this paper, we extend Jones' result -- that cons-free programming with -order data and a call-by-value strategy characterises EXPTIME -- to a more general setting, i…
Higher-order Cons-free Interpreters
Cynthia Kop, Jakob Grue Simonsen
Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot…
Quasi-reductivity of Logically Constrained Term Rewriting Systems
Cynthia Kop
This paper considers quasi-reductivity - essentially, the property that an evaluation cannot get "stuck" due to a missing case in pattern matching - in the context of term rewritin…
Termination of LCTRSs
Cynthia Kop
Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termina…
Complexity of Conditional Term Rewriting
Cynthia Kop, Aart Middeldorp, Thomas Sternagel
We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. This notion is realistic in the sense that it measures not only suc…
Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…
First-Order Formative Rules
Carsten Fuhs, Cynthia Kop
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, for…
Dynamic Dependency Pairs for Algebraic Functional Systems
Cynthia Kop, Femke van Raamsdonk
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reductio…
Polynomial Interpretations for Higher-Order Rewriting
Carsten Fuhs, Cynthia Kop
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recen…