TY - JOUR
T1 - A Rewriting Logic Approach to Operational Semantics (Extended Abstract)
AU - Şerbǎnuţǎ, Traian Florin
AU - Roşu, Grigore
AU - Meseguer, José
N1 - Funding Information:
1 Supported in part by NSF grants by ONR Grant N00014-02-1-0715.
PY - 2007/10/24
Y1 - 2007/10/24
N2 - 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.
AB - 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.
KW - operational semantics
KW - programming languages
KW - rewriting logic
UR - http://www.scopus.com/inward/record.url?scp=35448980371&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35448980371&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2007.08.020
DO - 10.1016/j.entcs.2007.08.020
M3 - Article
AN - SCOPUS:35448980371
SN - 1571-0661
VL - 192
SP - 125
EP - 141
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1 SPEC. ISS.
ER -