An Executable Rewriting Logic Semantics of K-Scheme

This paper presents an executable rewriting logic semantics of K-Scheme, a dialect of Scheme based (partially) on the informal defi-nition given in the R5RS report (Kelsey et al. 1998). The presented semantics follows the K language definitional style (Roşu 2005 and 2006) and is a pure rewriting logic specification (Meseguer 1992) containing 772 equations and 1 rewrite rule, so it can also be re-garded as an algebraic denotational specification with an initial model semantics. Rewriting logic specifications can be executed on common (context-insensitive) rewrite engines, provided that equa-tions are oriented into rewrite rules, typically from left-to-right. While in theory rewriting logic specifications can let certain behav-iors underspecified, thus allowing more models, in practice they need to completely specify all the desired behaviors if one wants to use their associated rewrite systems as “interpreters”, or “imple