Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)
Logic in Computer Science
2018-12-06 v1
Abstract
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.
Cite
@article{arxiv.1812.01853,
title = {Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)},
author = {Frédéric Blanqui and Guillaume Genestier},
journal= {arXiv preprint arXiv:1812.01853},
year = {2018}
}