An Isabelle/HOL-based model of stratego-like traversal strategies

Traversal strategies are at the heart of transformational programming with rewriting-based frameworks such as Stratego/XT or Tom and specific approaches for generic functional programming such as Strafunski or "Scrap your boilerplate". Such traversal strategies are distinctively based on one-layer traversal primitives from which traversal schemes are derived by recursive closure. We describe a mechanized, formal model of such strategies. The model covers two different semantics of strategies, strategic programming laws, termination conditions for strategy combinators as well as properties related to the success/failure behavior of strategies. The model has been mechanized in Isabelle/HOL.