Abstract
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed λ-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA. © Carsten Fuhs and Cynthia Kop.
Original language | English |
---|---|
Title of host publication | Proceedings of RTA '12 |
Editors | A. Tiwari |
Place of Publication | Dagstuhl, Germany |
Publisher | Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik |
Pages | 176-192 |
ISBN (Print) | 9783939897385 |
DOIs | |
Publication status | Published - 2012 |
Event | Rewriting Techniques and Applications - Dagstuhl, Germany Duration: 1 Jan 2012 → 1 Jan 2012 |
Conference
Conference | Rewriting Techniques and Applications |
---|---|
Period | 1/01/12 → 1/01/12 |