Lambda the Ultimate

This paper presents an operational semantics for the core of Scheme. Our specification improves over the existing R5RS denotational specification in four ways:

1. It is more complete, since it contains eval, quote, and dynamic-wind.
2. It models multiple values in a way that does not require changes to unrelated parts of the language.
3. It provides a more faithful model of Scheme's undefined order of evaluation.
4. It is executable, because it is encoded as a program in PLT Redex, a domain-specific language for writing operational semantics.

The executable specification 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 contributing a specification of Scheme, this paper presents several novel modeling techniques for Felleisen Hieb-style rewriting semantics that we discovered while developing our R5RS Scheme semantics. All are applicable to a wider range of problems than the specific uses we have for them, and the fact that they combine seamlessly in our full R5RS model shows that they scale to real languages.

This looks like excellent work, as we've come to expect from the PLT folk.

The PLT Redex tool was previously discussed on LtU. If you're interested in checking it out, this page provides links to "everything you need to run PLT Redex and executable versions of every reduction system in the paper".

Thanks to Jens Axel Søgaard for bringing this paper to my attention.