Talkmametjanov0311

Talk/Colloquium

Title: A Type Analysis of Rewrite Strategies

Speaker: Azamat Mametjanov (University of Nebraska at Omaha)

Host: Ralf Lämmel, Inst. for Software Technology and CS

Date/Time: 28 Mar 2011 (Monday), 5.00pm (ct)

Room: B 013

Abstract

Rule-based program transformation employs term rewriting strategies to algorithmically control rewrite sequences. The primary abstractions of rewriting strategies — rewrite rules, combinators and term traversals — provide basic yet powerful constructs enabling complex program transformation. Due to the programmability of rewrites, errors are often made because of incorrect compositions or incorrect applications of rewrites to a term within a strategic rewriting program. In practice, ill-formed strategies are the Achilles heel of strategic rewriting and present a major obstacle to the effective application of strategies to large complex problems. We propose a type analysis geared towards term rewriting strategies to detect and remove errors statically. Novel aspects of this analysis are (1) more precise type-checking enabled by the data type constructor-based typing of terms and patterns, and (2) integration of compositional behavior of strategies to model arguments and results of rewrite rule compositions. The primary benefit of such analysis is automated detection of ill-formed strategies, which in turn can significantly reduce the development and testing of program transformations. The analysis is demonstrated on TL — a representative transformation language supporting all of the strategic abstractions.

Biography

Azamat Mametjanov is a Ph.D. candidate in the College of Information Science and Technology at the University of Nebraska at Omaha. His research interests are in programming language design and implementation and language-based software engineering. His focus is in strategic rewriting that automates and scales programming tasks. His thesis introduced higher-precision types into static analysis of strategic programs to aid the development and validation of program transformations.