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.
https://hal.inria.fr/inria-00084821 Contributor : Frédéric BlanquiConnect in order to contact the contributor Submitted on : Monday, April 23, 2018 - 4:28:12 PM Last modification on : Friday, February 4, 2022 - 3:30:02 AM Long-term archiving on: : Tuesday, September 18, 2018 - 11:21:23 PM
Frédéric Blanqui. Higher-order dependency pairs. Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States. ⟨inria-00084821v3⟩