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. Categories and Subject Descriptors D.3.3 [PROGRAMMING

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Markus Kaiser, Ralf Lämmel
• Keywords: One-layer Traversal Primitives, PPDP 2009, Programming Languages, Such Traversal Strategies, Traversal Strategies