Checking a Denotational Semantics of Scheme in Agda

[Arthur A. Gleckler]

At the Scheme Workshop last week, Prof. Peter D. Mosses (CC-ed) gave an excellent talk on his work using Agda to check the denotational semantics of Scheme from R5RS.  I've attached his paper on the subject.  He did a careful analysis, and found some errors from R5RS that are probably still in R7RS Small.  I spoke with him after the talk, and he volunteered to help bring the denotational semantics up to date.

Thank you, Prof. Mosses.