Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)

CRI; ENS Paris Saclay); Fr\'ed\'eric Blanqui (DEDUCTEAM; Guillaume Genestier (DEDUCTEAM; LSV; LSV)

arxiv: 1812.01853 · v1 · pith:SLAE4O44new · submitted 2018-12-05 · 💻 cs.LO

Termination of λPi modulo rewriting using the size-change principle (work in progress)

Fr\'ed\'eric Blanqui (DEDUCTEAM , LSV) , Guillaume Genestier (DEDUCTEAM , LSV , CRI , ENS Paris Saclay) This is my paper

classification 💻 cs.LO

keywords terminationprinciplerewritingsize-changeworkdependentextendingfirst

0 comments

read the original 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.

This paper has not been read by Pith yet.

Termination of λPi modulo rewriting using the size-change principle (work in progress)

discussion (0)