[TYPES/announce] An operational semantics for Scheme, in PLT Redex

Robby Findler robby at cs.uchicago.edu
Fri Nov 9 17:12:16 EST 2007


As many of you know, the R6RS has recently been ratified by
the Scheme community. Along with a much larger language, the
Report now includes an operational semantics for a large
portion of the language including unspecified order of
evaluation, continuations and dynamic-wind, multiple values,
quote, exceptions, eqv, letrec, etc (the only major, missing
features are macros and the numeric tower).

The semantics is a Felleisen/Hieb-style reduction semantics
and is implemented in PLT Redex. The executable semantics
comes with a large test suite that helps to ensure the
semantics models the intended language.

A Journal of Functional Programming paper on the semantics
is about to appear (in addition to the semantics, it shows
how the individual features work in a series of smaller
calculi and how they combine seamlessly into the large
semantics).

 Draft JFP Paper:
 http://www.cs.uchicago.edu/~robby/an-operational-semantics-for-scheme/

 R6RS Report:
 http://www.r6rs.org/

This is joint work with Jacob Matthews.

Robby



More information about the Types-announce mailing list