Sciweavers

FROCOS
2011
Springer

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

12 years 3 months ago
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. Key words: higher order rewriting, termination, dependency pairs, modularity
Carsten Fuhs, Cynthia Kop
Added 22 Dec 2011
Updated 22 Dec 2011
Type Journal
Year 2011
Where FROCOS
Authors Carsten Fuhs, Cynthia Kop
Comments (0)