Termination of λΠ modulo rewriting using the size-change principle (work in progress), with Guillaume Genestier, 5 pages, 2018, submitted to WST'18.

The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types extending LF.

Statcounter W3C Validator Last updated on 27 June 2018. Come back to main page.