# A Rewriting Logic Approach to Operational Semantics

From FSL

## Information&Computation

**A Rewriting Logic Approach to Operational Semantics**- Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
, Volume 207(2), pp 305-340. 2009**Information and Computation**

*Abstract.*This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be*faithfully*captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

## SOS '07

**A Rewriting Logic Approach to Operational Semantics -- Extended Abstract**- Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
, ENTCS 192(1), pp 125-141. 2007**SOS'07**

*Abstract.*This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be*faithfully captured*as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

- PDF, Slides (PPT), ENTCS, SOS'07, BIB

## Technical Report

**A Rewriting Logic Approach to Operational Semantics**- Traian Florin Serbanuta and Grigore Rosu
UIUCDCS-R-2006-2780, October 2006**Technical Report**

*Abstract.*We show how one can use rewriting logic to*faithfully capture*(not implement) various operational semantic frameworks as rewrite logic theories, namely big-step and small-step semantics, reduction semantics using evaluation contexts, and continuation-based semantics. There is a one-to-one correspondence between an original operational semantics and its associated rewrite logic theory, both notationally and computationally. Once an operational semantics is defined as a rewrite logic theory, one can use standard, off-the-shelf context-insensitive rewrite engines to ``execute'' programs directly within their semantics; in other words, one gets*interpreters for free*for the defined languages, directly from their semantic definitions. Experiments show that the resulting correct-by-definition interpreters are also reasonably performant.