The Scheme programming language was introduced in 1975 as a lexically-scoped dialect of Lisp. It has subsequently been improved and extended through many rounds of standardization, documented by the Scheme Reports.

In Lisp, eval is a function taking a single argument; when the value of the argument represents an expression, eval proceeds to evaluate it in the current environment. The Scheme procedure eval is similar, but takes an extra argument that determines the evaluation environment.

The so-called classic standards for Scheme and its latest modern standard all include a denotational semantics of core expressions and of some required procedures. However, the semantics does not cover eval. When Muchnick and Pleban compared the denotational semantics of Lisp and Scheme in 1980, they wrote that it was not possible to give a structural semantics of eval expressions. Similarly, in 1984, Clinger pointed out that the semantics of \texttt{eval} violates compositionality; he suggested to define eval using a non-compositional copy of the semantic function.

This paper adapts Clinger’s suggestion by letting the semantic function take an extra argument, then defining that argument by an explicit fixed point. The resulting semantics of eval expressions is fully compositional. The wellformedness of the semantics has been tested using a lightweight Agda formalization; verifying that the denotations have expected properties is work in progress.

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.