Denotational Semantics in Agda
Table of Contents
This project (started in 2024) aims to make it straightforward to take an existing denotational semantics of a programming language, and use the Agda type-checker to test its well-formedness. A secondary aim is to test whether the denotations of individual programs have expected properties.
The Problem #
A Scott–Strachey style denotational semantics1 is based on Scott-domains. It assumes that a domain is an appropriate kind of cpo, and defines domains (up to isomorphism) using various domain constructors, allowing mutual recursion. All functions on domains specified in λ-notation are Scott-continuous, and endofunctions have least fixed points.
Agda does not assume that types are Scott-domains, nor that functions specified in λ-notation are continuous. Some Agda libraries have been developed to support Scott-domains; but when using them, a domain is represented as a pair of a type of elements and other data; and a continuous function is represented as a pair of a function and a proof of its continuity. These representations give rise to undesirable notational overhead and obfuscation when specifying elements of domains in λ-notation.
Experiments #
As a novice Agda user, I experimented with a lightweight workaround for this problem, reported in
Towards Verification of a Denotational Semantics of Inheritance (JENSFEST 2024),
Lightweight Agda Formalization of Denotational Semantics (TYPES 2025),
Checking a Denotational Semantics of Scheme in Agda (SCHEME 2025), and
*A Compositional Semantics for eval in Scheme *(OlivierFest 2025).
Some experiments with using a simplified version2 of the above approach are documented at https://pdmosses.github.io/xds-agda/. The experiments currently include Agda formalizations of the denotational semantics of the untyped λ-calculus, PCF, and Scm (a simple sublanguage of Scheme). These experiments are reported in *Mechanising Denotational Semantics in Agda*, with Jesper Cockx and Bernhard Reus (MFPS 2026). See the accompanying website and slides.
The lightweight approach simply assumed that some Agda types are Scott-domains, and that all Agda functions between domains have fixed points. Such assumptions are unsound, but the Agda proof assistant accepted them, and their unsoundness did not affect checking definitions for well-formedness.
However, it would clearly be better to develop a more principled solution, based on an implementation of Synthetic Domain Theory (SDT) in Agda. The assistance of expert Agda users will surely be needed…
A denotational semantics of a programming language maps programs and their phrases directly to their denotations: immutable values – typically higher-order functions. The denotation of a complete program represents its potential behaviour when executed. Denotations are compositional: the denotation of a phrase is defined inductively in terms of the denotations of its subphrases, independently of their form. The denotations of loops and recursive definitions involve fixed points of functions on denotations. ↩︎
For simplicity, domains are defined to be unordered pointed sets, and endofunctions are required only to have well-defined fixed points. Postulates corresponding to the intended cpo structure of domains, and the continuity of functions between domains, are to be added. ↩︎