Typed generic traversals in $S_gamma^'$

A typed model of strategic rewriting is developed. An innovation is that generic traversals are covered. To this end, we define a rewriting calculus $S'_{gamma$. The calculus offers a few strategy combinators for generic traversals. There is, for example, a combinator to apply a strategy to all immediate subterms of a given term. This idiom is relevant for generic type-preserving traversals. We also go beyond type-preservation which corresponds to another innovation. There is, for example, a combinator to reduce all the immediate subterms of a term. $S'_{gamma$ employs a many-sorted type system extended by distinguished signature-independent (say generic) strategy types $gamma$. To inhabit generic types, we need to add a fundamental combinator to lift a many-sorted strategy $s$ to a generic type $gamma$. The reduction semantics for this kind of lifting states that $s$ is only applied if the type of the term at hand fits, otherwise the strategy fails. This approach dictates that the semantics of strategy application must be type-dependent to a certain extent. Typed strategic rewriting with generic traversals is a simple but expressive model of generic programming. It has applications in program transformation and program analysis.