Talk: Strategies and simulations in a semantic framework
- Local: Fundação Pe. Leonel Franca
- Date: 25, September 2006 at 11 hours
Rewriting logic provides a semantic framework in which we can express different languages and models of computation. The paper Rewriting logic as a logical and semantic framework (with José Meseguer) studies the representation of several operational semantics in rewriting logic. Alberto Verdejo's PhD thesis extends this idea of semantic framework to the one of executable semantic framework, obtaining executable representations of different operational semantics.
The declarative language Maude, based on rewriting logic, becomes a metalanguage to specify different kinds of languages; it is very useful to develop executable prototypes of different kinds of systems. In particular, Maude's use as a metalanguage allows the definition of operational semantics for programming and specification languages. However, because of the need to control the execution of some rules, it is very convenient to have a strategy language that allows a simpler definition of the behavior of many systems, as well as of the semantics of more or less complex languages.
This talk summarizes a proposal for such a strategy language and presents a prototype implemented in Maude itself, which has been used in several case studies, including a semantics for the parallel functional language Eden, in which strategies play an essential role. Currently we are redesigning this strategy language with the aim of incorporating the language at the level of the rewrite engine of Maude, and validating it with new case studies.
Another dimension studied in the context of rewriting logic as a semantic framework is the way to establish relationships between systems, for example, to relate semantics that operate at different levels of atomicity. The concept of stuttering simulation provides a mathematical foundation for this kind of relationship. In the second part of this talk we introduce several concepts of simulations and show some results about them. Miguel Palomino's PhD thesis (supervised jointly with José Meseguer) studies many other aspects related to simulations.
Prof. Narciso Martí-Oliet is "Professor Titular" at the Facultad de Informática of the Universidad Complutense de Madrid and head of the Maude group. Prof. Martí-Oliet has been working on Rewriting Logic and the Maude system for several years with many contributions in this research area, in particular on Rewriting Logic as a logical and semantic framework. His current research interests are on the development and application of a strategy language for the Maude system and on the development of a mathematical foundation for comparing specifications in Rewriting Logic.