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.

The following highlighted listings of the code were generated using Agda.

• Modules: hyperlinked web pages of the formalization

• Library: hyperlinked web pages of imported standard Agda library modules

• HTML: the hyperlinked HTML pages generated by Agda

• PDF: a PDF listing of the formalization