PLT Redex operational semantics for Scheme

(via the TYPES Forum)

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


The paper actually covers the operational semantics for R5RS, extending their earlier Scheme Workshop paper on the semantics of R5RS.

For R6RS...

The R6RS semantics for PLT Redex are available here.


I double checked what digit I put in, but I was sure I am posting the mistaken report number, which indeed I was... Thanks, guys.