An Isabelle/HOL-based model of Stratego-like traversal strategies
Status
Paper published in PPDP'09 proceedings.
Paper and Isabelle/HOL theories available online.
Authors
Markus Kaiser and Ralf Lämmel
Abstract
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.
@inproceedings{MetaStrategoTheory,
author = "Markus Kaiser and Ralf L{\"a}mmel",
title = "{An Isabelle/HOL-based model of Stratego-like traversal strategies}",
booktitle = "{PPDP'09 Proceedings}",
publisher = "ACM",
year = 2009,
}