Rewriting Logic Semantics Readings

From FSL

Jump to: navigation, search

These papers provide background on using rewriting logic to specify the semantics of programming languages. Papers covering the general approach, our context-based approach, and alternate approaches are all presented. Additional papers will be added going forward.

[edit] Rewriting Logic Semantics for Languages

  • Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools -- Meseguer and Rosu

http://citeseer.ist.psu.edu/meseguer04rewriting.html or http://springerlink.metapress.com/link.asp?id=dkxbq24xb8k967ac This provides an overview of the use of rewriting logic to specify the semantics of programming languages and language calculi. The focus is on rewriting logic in general, so while it discusses our technique it does not focus on it. I believe this is the first paper that specifically mentions our continuation-based technique.

http://fsl.cs.uiuc.edu/~grosu/download/sos05.pdf This is an update to the prior paper, taking account of research which had occured during the intervening time. This presents more information on rewriting logic semantics, and includes some more up-to-date versions of our method of language specification in Maude (but not yet in K). The references in both this and the prior paper are a good place to go for more information about specific topics, as well.

[edit] The Continuation-Based Approach and K

This paper, available on the KOOL language page, uses K to define a fair chunk of KOOL, a simple OO loosely based on Smalltalk (class-based, single inheritance, dynamically typed), and Java. The appendix provides a good introduction to rewriting logic.

This paper, available on the SILF language page, uses K to define almost all of the Simple Imperative Language with Functions (only some infrastructure-type stuff, like updating the environment, is left out). It also touches on our work to turn these language definitions into efficient interpreters via compilation into an underlying language such as C which has good performance properties.

http://citeseer.ist.psu.edu/farzan04formal.html This is a definition of a subset of Java in Maude. A companion paper, at http://citeseer.ist.psu.edu/696210.html, deals with the definition of the JVM in Maude, but doesn't use our continuation-based style.

[edit] Alternate Approaches

  • Plan in Maude: Specifying an Active Network Programming Language -- Stehr and Talcott

http://citeseer.ist.psu.edu/stehr02plan.html This paper presents a definition of the Plan language in Maude. It is an interesting example of using Rewriting Logic Semantics to define a language but not using our continuation-based method.

  • Executable Structural Operational Semantics in Maude -- Verdejo and Marti-Oliet

http://citeseer.ist.psu.edu/verdejo03executable.html This uses language definitions in SOS which can then be manipulated by Maude. A newer paper, which I don't belive is online, provides an executable MSOS engine where languages defined in MSOS can then be executed.

Retrieved from "http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_Readings"
Views