An operational semantics for Scheme

Jacob Matthews*, Robert Bruce Findler

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

10 Scopus citations


This paper presents an operational semantics for the core of Scheme. Our specification improves over the denotational semantics from the Revised5 Report on Scheme specification in four ways. First, it covers a larger part of the language, specifically eval, quote, dynamic-wind, and the top level. Second, it models multiple values in a way that does not require changes to unrelated parts of the language. Third, it provides a faithful model of Scheme's undefined order of evaluation. Finally, we have implemented our specification in PLT Redex, a domain-specific language for writing operational semantics. The implementation allows others to experiment with our specification and allows us to build a specification test suite, which improves our confidence that our system is a faithful model of Scheme. In addition to a specification of Scheme, this paper contributes three novel modeling techniques for Felleisen Hieb-style rewriting semantics. All three techniques are applicable to a wider range of problems than modeling Scheme, and they combine seamlessly in our model, suggesting that they would scale to complete models of other languages.

Original languageEnglish (US)
Pages (from-to)47-86
Number of pages40
JournalJournal of Functional Programming
Issue number1
StatePublished - Jan 2008

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'An operational semantics for Scheme'. Together they form a unique fingerprint.

Cite this