2 papers
cs.LO2019
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this tech…
cs.LO2018
Termination of modulo rewriting using the size-change principle (work in progress)
Frédéric Blanqui, Guillaume Genestier
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…