Scheme semantics in Maude

I just stumbled on some work that's related to the R5RS operational semantics paper I wrote recently. Right at about the same time I was doing that, some folks on the Maude team did a Maude-based rewriting semantics for Scheme also, and wrote a paper about it for the Brazilian Symposium on Programming Languages called "An Equational Specification for the Scheme Language" (source code). It looks like they didn't model the two things that gave me the most trouble (unspecified order-of-evaluation and multiple values). Also, they're excited about the fact that their model of call/cc is so small, but that's because their entire system is in CPS style ...

Anyway, it's interesting to compare their system to ours and see how our different priorities led to different systems. For instance they've got an entire section on performance metrics. Performance was explicitly a non-goal for us. If our paper had a section on performance, it would read something like: "We were able to compute (fib 7) in, like, an hour or so."