35 citations · 80 across the 25 of their papers we have counts for
27 papers
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…
Tuple Interpretations for Higher-Order Rewriting
Deivid Vale, Cynthia Kop
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are…
Cons-free Programs and Complexity Classes between LOGSPACE and PTIME
Neil D. Jones, Siddharth Bhaskar, Cynthia Kop +1
Programming language concepts are used to give some new perspectives on a long-standing open problem: is logspace = ptime ?
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…
h: A Plank for Higher-order Attribute Contraction Schemes
Cynthia Kop, Kristoffer Rose
We present and formalize h, a core (or "plank") calculus that can serve as the foundation for several compiler specification languages, notably CRSX (Combinatory Reductions Systems…
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…
The Power of Non-Determinism in Higher-Order Implicit Complexity
Cynthia Kop, Jakob Grue Simonsen
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders,…
Complexity Hierarchies and Higher-order Cons-free Term Rewriting
Cynthia Kop, Jakob Grue Simonsen
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuit…
Complexity Hierarchies and Higher-Order Cons-Free Rewriting
Cynthia Kop, Jakob Grue Simonsen
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the…
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…