Strategies and User Interfaces in Maude

Manuel Clavel (Universidad Complutense de Madrid, Spain)

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities. We explain and illustrate with examples two of these reflective features: user-definable declarative strategies and user-definable declarative interfaces. We conclude with an application, namely, an inductive theorem prover, whose implementation effectively combines both reflective features.

Rewrite Strategies in the Rewriting Calculus

Claude Kirchner (LORIA - INRIA Lorraine, France)

This talk presents an overview on the use of the rewriting calculus to express rewrite strategies. We motivate first the use of rewrite strategies by examples in the ELAN language. We then show how this has be modelled in the initial version of the rewriting calculus and how the matching power of this framework facilitates the writing of powerful strategies.