A Rewriting Logic Approach to Operational Semantics
From FSL
(Redirected from A Rewriting Logic Approach to Operational Semantics -- Extended Abstract)
[edit] Information&Computation
- 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, DOI, BIB
[edit] SOS '07
- 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, SOS'07 Slides, ENTCS, SOS'07, BIB
[edit] Technical Report
- 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.
