3 papers
cs.LO2023
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…
cs.LO2022
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…
cs.LO2021
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…