Dynamic dependency pairs for algebraic functional systems

Publikation: Bidrag til tidsskriftTidsskriftartikelfagfællebedømt

  • Cynthia Louisa Martina Kop
  • Femke van Raamsdonk
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate beta-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.
OriginalsprogEngelsk
Artikelnummer10
TidsskriftLogical Methods in Computer Science
Vol/bind8
Udgave nummer2
Antal sider51
ISSN1860-5974
StatusUdgivet - 2012
Eksternt udgivetJa

ID: 148058703