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

9 years 22 days ago
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
Markus Kaiser, Ralf Lämmel
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where PPDP
Authors Markus Kaiser, Ralf Lämmel
Comments (0)