A Rewriting Logic Approach to Operational Semantics

From FSL
Jump to: navigation, search

Information&Computation

A Rewriting Logic Approach to Operational Semantics
Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
Information and Computation, Volume 207(2), pp 305-340. 2009
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.
PDF, Experiments, J.Inf.&Comp., BIB

SOS '07

A Rewriting Logic Approach to Operational Semantics -- Extended Abstract
Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
SOS'07, ENTCS 192(1), pp 125-141. 2007
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
Technical Report UIUCDCS-R-2006-2780, October 2006
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.
Extended Version, Experiments, PDF, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation