Higher-order dependency pairs
Logic in Computer Science
2018-04-25 v1
Abstract
Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its "dependency pairs". We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.
Keywords
Cite
@article{arxiv.1804.08855,
title = {Higher-order dependency pairs},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:1804.08855},
year = {2018}
}