Operational Semantics for Scheme via Term Rewriting

Jacob Matthews. 8 April, 2005.
Communicated by Robby Findler.


Felleisenís notion of context-sensitive term rewriting systems a flexible tool for specifying operational semantics, but one that requires great care to use properly. We introduce PLT Redex, a program for exploring context-sensitive rewriting systems as executable specifications that makes using Felleisenís systems easier and less error-prone and allows researchers to apply software engineering principles to formal semantics systems. We also present an operational semantics for R5RS Scheme encoded in PLT Redex that is to our knowledge the first operational semantics for R5RS Scheme that covers the entire report and the most complete formal encoding of the languageís semantics given in any style.

Original Document

The original document is available in PDF (uploaded 8 April, 2005 by Robby Findler).