A Formal Rewriting Logic Semantic Definition of Scheme

Meredith, Patrick O'Neil; Hills, Mark; Rosu, Grigore

Permalink

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

Description

Title

A Formal Rewriting Logic Semantic Definition of Scheme

Author(s)

• Meredith, Patrick O'Neil
• Hills, Mark
• Rosu, Grigore

Issue Date

2007-07

Keyword(s)

computer science

Abstract

This paper presents a formal definition of Scheme (based on the informal definition given in the R5RS report R5RS. The definition is purely equational, so it can be regarded as an algebraic denotational specification with an initial model/algebra semantics of Scheme. Moreover, it is executable, in the sense that equations can be oriented from left-to-right into rewrite rules and thus giving an operational semantics of Scheme as well; this way, an interpreter for Scheme is obtained for free by just executing the presented Scheme definition on term rewrite engines. Maude is used in this paper, but other equational engines could have been used as well. The definition in this paper is the most complete formal definition of Scheme that we are aware of and can play two important roles: as a formal definition of Scheme complementary to the informal one in the R5RS report, and as a platform for experimentation with variants and extensions of Scheme, for example concurrency. This work is part of the rewriting logic semantics project, whose broad scope is to formally define languages and language features in rewriting logic, and then use the generic support provided by rewriting logic to obtain not only interpreters, but also formal analysis tools for the defined languages.

Type of Resource

text

Permalink

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

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