The authoritative standards for the algorithmic language Scheme are the Scheme reports. Most of the revised reports include a denotational semantics for primitive Scheme expressions and selected procedures.

This paper first traces the history of the semantic definition, and summarizes its form and content. It then presents a shallow embedding of denotational semantics into the functional programming language Agda. The embedding is illustrated by showing how fragments of the denotational semantics given in the fifth revised Scheme report (R⁵RS) are embedded into Agda.

Type-checking the Agda embedding of a semantics indirectly tests its wellformedness. Agda reported several issues with the embedding of the complete denotational semantics from R⁵RS. The paper suggests changes to the semantics that would address the reported issues, as well as further changes that could improve the conciseness and perspicuity of the definitions.

This paper is dedicated to the memory of Christopher Strachey (1916–1975)

Peter Mosses is professor emeritus at Swansea University, and currently visiting the Programming Languages Group at Delft University of Technology.

His research in semantics stretches back to Christopher Strachey’s Programming Research Group at Oxford in the early 1970s, where he contributed to the development of denotational semantics, and implemented SIS, a system for running programs based on their semantics. He was based at Aarhus University, Denmark, from 1976 to 2004.

The main focus of his research has been on pragmatic aspects of formal specifications – especially modularity. This led to the development of action semantics, MSOS (a modular variant of structural operational semantics) and component-based semantics. He is a principal investigator in the PLanCompS project (Programming Language Components and Specifications), He was also the initial coordinator of CoFI, the Common Framework Initiative, which designed the algebraic specification language CASL.