More Precise Typing of Rewrite Strategies

Forward declaration
Please visit the following site for supplementary material: [.html] (maintained by Azamat Mametjanov)
Status
To appear in proceedings of LDTA 2011

Authors
Azamat Mametjanov, Victor Winter, and Ralf Lämmel

Abstract
The programming concept of rewrite strategies supports versatile composition of rewrite rules and control of their application. Such programmability of rewrites can possibly lead to incorrect compositions of rewrites or incorrect applications of rewrites to terms within a strategic rewriting program. In this paper, we explore the analysis of strategic rewriting programs to detect certain programming errors statically. In particular, we introduce fine-grain types to closely approximate the dynamic behavior of rewriting. We develop an expressive type system for a core rewriting language. The resulting system detects programming errors of universally unreachable and failing rewrites. Static detection of such errors can substantially reduce testing and debugging efforts and lead to a more effective use of strategic rewriting in large and complex rewriting problems.

Bibtex entry
@inproceedings{APIREP,
 author = "Azamat Mametjanov and Victor Winter and Ralf L\"ammel",
 title = "{More Precise Typing of Rewrite Strategies}",
 booktitle = "{11th International Workshop on Language Descriptions, Tools, and Applications (LDTA 2011)}",
 publisher = "ACM",
 year  = 2011,
 month = mar,
 note  = "8 pages"
}

Downloads and links