Abstract We provide a general and modular criterion for the termination of simply typed λ-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.

@article{paperbot336,
  title = {Size-based termination of higher-order rewriting},
  author = {FRÉDÉRIC BLANQUI},
  journal = {Journal of Functional Programming},
  volume = {28},
  year = {2018},
  doi = {10.1017/s0956796818000072}
}