Mechanising Denotational Semantics in Agda

Peter D. Mosses; Jesper Cockx; Bernhard Reus

Home/Archive/arXiv

arXiv · 2610.14898

Mechanising Denotational Semantics in Agda

Peter D. Mosses·Jesper Cockx·Bernhard Reus

View original source ↗Read source document ↗Export metadata ↓

Abstract

Mechanisation of a mathematical definition (also referred to as formalisation) has many benefits. Here, we focus on mechanising denotational semantic definitions of programming languages by embedding them in the Agda language. The Agda type-checker detects and reports any issues with the wellformedness and type correctness of the embedded definitions. To minimise the effort required, and to facilitate correlation of the original definition with its Agda embedding, mechanisation should not involve significant reformulation or extension. Here, we show how to embed conventional Scott-Strachey denotational definitions in Agda with almost no changes to $λ$-notation or domain equations. Agda notation for definitions of types and functions corresponds closely to the conventional meta-notation of denotational semantics. We have developed a collection of Agda modules with postulated types for commonly used domain constructors and their associated operations. We illustrate our approach with mechanisations of three denotational definitions: a model of the untyped $λ$-calculus, Plotkin's denotational semantics of PCF, and a semantics of a sublanguage of Scheme. In previous work, similar mechanisations in Agda have revealed several unsuspected wellformedness issues in published denotational definitions. Some of the postulated properties of our definitions are inconsistent with a classical set-theoretic interpretation of Agda. We conjecture that they would be consistent with an interpretation of Agda in a higher-order intuititionistic logic, such as that used by Simpson in his work on synthetic domain theory. After recalling previous work on mechanising domain theory, we consider the possibility of mechanising synthetic domain theory in Agda.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Peter D. Mosses, Jesper Cockx, Bernhard Reus. 2026-10-10. Mechanising Denotational Semantics in Agda. https://arxiv.org/abs/2610.14898

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

FlowBook: Enforcing Reproducibility in Computational Notebooks

Computational notebooks interleave code cells with their outputs and let users edit and execute cells in arbitrary order. This flexibility supports interactive exploration, but it also allows outputs to become inconsistent with the notebook's current code and data. Such inconsistencies can lead users to draw invalid scientific conclusions. We argue that notebooks should always be output consistent: every output should match what a top-to-bottom execution of the current code would produce. Forcing a top-to-bottom execution after each edit would guarantee this, but at prohibitive cost: such an execution can take minutes to hours. We present FlowBook, a dynamic analysis for Python notebooks that enforces output consistency without giving up out-of-order execution. FlowBook does this by enforcing a stronger property, rerun consistency: no location read by a cell may be written by any cell below it. Rerun consistency guarantees that rerunning a cell later, in any order, reproduces its current output. FlowBook tracks each cell's read and write sets at cell boundaries, blocks updates that would violate rerun consistency, and marks as stale any cell whose inputs may have changed. We prove that a notebook with no stale cells is both rerun and output consistent. Users remain free to execute cells in arbitrary order; the only restriction is that recorded outputs may not silently depend on the order in which cells were executed. Across 61 real-world notebooks, FlowBook flagged 203 rerun-inconsistent cells. Rerunning 62% led to output inconsistencies. A further 21% change notebook state with no visible output, which can affect the results of later edits and reruns; only 5% are false positives of FlowBook's conservative analysis. FlowBook's AI repair agent repaired all 203 cells with local edits and no human intervention. FlowBook's median overhead is only 26 ms per cell execution.

cs.PL↗

arXiv2026

From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

Enforcing invariants in safety-critical firmware is increasingly urgent as generated code becomes widespread, but standard extraction targets for proof assistants require runtimes too large for many embedded devices. We present a pipeline for running formally verified Rocq firmware logic on Cortex-M microcontrollers. The pipeline extracts Gallina to Scheme, compiles it with Encore!, a bare-metal Continuation-Passing Style (CPS) bytecode virtual machine, and embeds the result in no_std Rust firmware. We structure applications as pure state-transition functions, so the business logic is proved in Rocq while the event/effect boundary, host callbacks, compiler, and VM remain explicit trusted components: no proof yet relates bytecode execution to Gallina semantics. On eight firmware workloads, from APDU parsing to a credential store, Encore! runs unmodified Rocq-extracted code within the 50 KiB RAM budget of ST33-class targets on every input size, where CertiRocq's generated code runs out of memory on the larger ones, at the price of up to 10 times more executed instructions than CertiRocq; a transaction-signing application is validated on physical Ledger Flex hardware.

cs.PL↗

arXiv2026

Compositional Information Geometry of Probabilistic Programs

We study the compositional, intensional information geometry of probabilistic programs. For a first-order probabilistic programming language with finite random variables, we construct a contravariant lax monoidal functor that, for a program of type $X \to Y$, pulls back a (degenerate) Riemannian metric on $Y$ to $X$. It specialises to the Fisher metric in the case of standard statistical models and to ordinary pullback in the case of deterministic programs. We further justify this construction in two ways. First, we show that this functor arises as a pullback of geometry from a universal space of programs over a type $Y$ with a fixed trace space. Second, we show that it is a special case of a more general pullback construction over weighted measures. Our compositional geometry depends on the presentation of the program, and we study how it relates to the (non-compositional) geometry of the realised measures by establishing a three-level inequality relating our score-velocity metric for the program, the program's corresponding output-conditioned metric, and the standard Wasserstein-Fisher-Rao metric of the realised family. Finally, we show how the theory can be extended to accommodate continuous random variables using diffeological quasi-Borel spaces. We also discuss several concrete directions for future work.

cs.PL↗