Order-sorted dependency pairs

Salvador Lucas, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Types (or sorts) are pervasive in computer science and in rewriting-based programming languages, which often support subtypes (sub-sorts) and subtype polymorphism. Programs in these languages can be modeled as order-sorted term rewriting systems (OS-TRSs). Often, termination of such programs heavily depends on sort information. But few techniques are currently available for proving termination of OS-TRSs; and they often fail for interesting OS-TRSs. In this paper we generalize the dependency pairs approach to prove termination of OS-TRSs. Preliminary experiments suggest that this technique can succeed where existing ones fail, yielding easier and simpler termination proofs.

Original languageEnglish (US)
Title of host publicationPPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
Pages108-119
Number of pages12
DOIs
StatePublished - Dec 17 2008
EventPPDP 2008: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - Valencia, Spain
Duration: Jul 15 2008Jul 17 2008

Publication series

NamePPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming

Other

OtherPPDP 2008: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
CountrySpain
CityValencia
Period7/15/087/17/08

    Fingerprint

Keywords

  • Program analysis
  • Term rewriting
  • Termination

ASJC Scopus subject areas

  • Computer Science Applications
  • Software

Cite this

Lucas, S., & Meseguer, J. (2008). Order-sorted dependency pairs. In PPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (pp. 108-119). (PPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming). https://doi.org/10.1145/1389449.1389463