Dynamic dependency pairs for algebraic functional systems
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Dynamic dependency pairs for algebraic functional systems. / Kop, Cynthia Louisa Martina; van Raamsdonk, Femke.
In: Logical Methods in Computer Science, Vol. 8, No. 2, 10, 2012.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Dynamic dependency pairs for algebraic functional systems
AU - Kop, Cynthia Louisa Martina
AU - van Raamsdonk, Femke
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
M3 - Journal article
VL - 8
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
SN - 1860-5974
IS - 2
M1 - 10
ER -
ID: 148058703