Lambda the Ultimate

R6RS 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 are Felleisen/Hieb-style reduction semantics and are implemented in PLT Redex.

A draft JFP paper describing operational semantics for R5RS and the reduction systems themselves are both available online courtesy of Jacob Matthews and Robert Findler.