The Rewriting Logic Semantics Project

From FSL
Jump to: navigation, search

This work has been published in a journal paper (J. of TCS), in a workshop proceedings (SOS'05) and in a technical report. These papers give an overview of the Rewriting Logic Semantics project as of the end of 2005, beginning of 2006. A language called SIMPLE is defined in rewriting logic using Maude; see the Experiments link in the technical report for its definition and several formal analysis experiments.

J. of TCS

The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Rosu
J. of TCS, Volume 373(3), pp 213-237. 2007
Abstract. Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory's axioms include both equations and rewrite rules provides a useful abstraction dial to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.
PDF, J.TCS, BIB

SOS'05

The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Rosu
SOS'05, ENTCS 156, pp. 27-56. 2006
Abstract. Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact that a rewrite theory's axioms include both equations and rewrite rules provides a very useful abstraction knob to find the right balance between abstraction and observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.
PDF, SOS'05, BIB

Technical report

The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Rosu
Technical Report UIUCDCS-R-2005-2639, September 2005
Abstract. Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact that a rewrite theory's axioms include both equations and rewrite rules provides a very useful abstraction knob to find the right balance between abstraction and observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.
PDF, Experiments, TR @ UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation