Mechanising Denotational Semantics in Agda
Agda code accompanying the final version of a paper presented at MFPS 2026:
Peter D. Mosses, Jesper Cockx, Bernhard Reus: Mechanising Denotational Semantics in Agda
Info
The Agda code presented in the preliminary version of the paper (PDF) is available in the preliminary branch of the mfps2026-agda repository. A build of the preliminary website generated from it has been added as a subdirectory of the current website.
Navigation
In Agda code blocks, clicking on a name jumps to its declaration.
When scrolling up, a back to top button appears.
Wide displays
The top panel of each page shows a row of tabs:
- About – the present page, and pages summarising Background and Meta-notation
- Notation – postulated types for domain constructors and associated operations
- Examples - shallow embeddings of denotational definitions
- Properties – postulated equivalences for operations
- Tests - some proven equivalences of denotations
- Library – modules imported from the standard Agda library (v2.3)
It also shows:
- pdmosses/mfps2026-agda – a link to the code repository
- a toggle between light, dark, and automatic modes
- a search field
The left sidepanel shows the navigation hierarchy.
When there is more than one level of navigation, clicking the expander icon
> for a section reveals links to its next level.
The right sidepanel shows links to any subsections of the current page.
Narrow displays
The window may show only the navigation hierarchy button and the search button.
Contributing
Please report any issues that you notice.
Comments and suggestions for improvement are welcome, and can be added as Discussions.
Contact
Peter Mosses