2 citations · 2 across the 7 of their papers we have counts for
8 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 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…
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…
Analyzing Innermost Runtime Complexity Through Tuple Interpretations
Liye Guo, Deivid Vale
Time complexity in rewriting is naturally understood as the number of steps needed to reduce terms to normal forms. Establishing complexity bounds to this measure is a well-known p…
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…
Formalizing Higher-Order Termination in Coq
Deivid Vale, Niels van der Weide
We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we…
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…