A Formal Rewriting Logic Semantic Definition of Scheme
Patrick Meredith, Mark Hills, Grigore Roşu · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2007
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.