A Rewriting Logic Approach to Operational Semantics

Serbanuta, Traian Florin; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11265 Copy

Description

Title

A Rewriting Logic Approach to Operational Semantics

Author(s)

• Serbanuta, Traian Florin
• Rosu, Grigore

Issue Date

2006-10

Keyword(s)

computer science

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 efficient.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11265

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections