A Sublanguage of Scheme

Scm is a particularly basic sublanguage of the core Scheme expressions whose denotational semantics is defined in the Scheme reports.

A denotational semantics for Scm is defined in the following paper:

Peter D. Mosses. 2025. A Compositional Semantics for eval in Scheme. In Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST ’25), October 12–18, 2025, Singapore, Singapore. ACM, New York, NY, USA, 10 pages. DOI

The Agda code of a lightweight formalization of the denotational semantics of Scm is available on GitHub.

See Scm for hyperlinked, highlighted listings of the code, generated using Agda-Material.