Files in this item

FilesDescriptionFormat

application/pdf

application/pdfA Formal Rewrit ... c Definition of Scheme.pdf (234kB)
(no description provided)PDF

Description

Title:A Formal Rewriting Logic Semantic Definition of Scheme
Author(s):Meredith, Patrick O'Neil; Hills, Mark; Rosu, Grigore
Subject(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.
Issue Date:2007-07
Genre:Technical Report
Type:Text
URI:http://hdl.handle.net/2142/11368
Other Identifier(s):UIUCDCS-R-2007-2877
Rights 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).
Date Available in IDEALS:2009-04-22


This item appears in the following Collection(s)

Item Statistics