Friday 8 April 2016, 10:30: Size-based termination for higher-order rewriting (2nd part), Frédéric Blanqui (Inria).

At POPL'96, Hughes, Pareto and Sabry presented an approach to the termination of closed ML-like programs based on type-checking and the abstract interpretation of a semantic notion of size. This approach was then extended by several authors to open terms and more complex type systems. In the first part, I will show how it can be extended in other directions: arbitrary user-defined notions of size and rewriting-based function definitions. In the second part, I will show how the decidability of type-checking (with size-induced subtyping) can be reduced to the existence, in the size algebra, of a smallest solution for any solvable set of inequalities, and show it for the successor algebra (which is enough to subsume Coq termination checker for instance).