Selected publications at LSV

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{B-jfp18,
   author = {Blanqui, Fr{\'e}d{\'e}ric},
   DOI = {10.1017/S0956796818000072},
   journal = {Journal of Functional Programming},
   month = apr,
   publisher = {Cambridge University Press},
   title = {Size-based termination of higher-order rewriting},
   url = {https://www.cambridge.org/core/journals/journal-of-functional-programming/article/sizebased-termination-of-higherorder-rewriting/2134D9160988448FA62DD693D337892D},
   volume = {28},
   year = {2018},
}

About LSV

Select by Year