Reference. Modelling Recursion and Probabilistic Choice in Guarded Type Theory

Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Annebet Zwart, Alejandro Aguirre, Lars Birkedal · POPL · 2025 · guarded-domain-theory guarded-recursion probabilistic · DOI · arXiv · pldb
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about FPC ⊕ , a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics of FPC ⊕ , as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.

Cite
Cite as @stassen-2025-modelling (helia, typst) · \cite{stassen-2025-modelling} (LaTeX)
BibTeX
bibtex · 1 line
@article{stassen-2025-modelling, title={Modelling Recursion and Probabilistic Choice in Guarded Type Theory}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3704884}, DOI={10.1145/3704884}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Stassen, Philipp and Møgelberg, Rasmus Ejlers and Zwart, Maaike Annebet and Aguirre, Alejandro and Birkedal, Lars}, year={2025}, month=Jan, pages={1417–1445} }
hayagriva YAML (typst)
yaml · 21 lines
stassen-2025-modelling:
  type: article
  title: Modelling Recursion and Probabilistic Choice in Guarded Type Theory
  author:
  - Stassen, Philipp
  - Møgelberg, Rasmus Ejlers
  - Zwart, Maaike Annebet
  - Aguirre, Alejandro
  - Birkedal, Lars
  date: 2025-01
  page-range: 1417-1445
  url: http://dx.doi.org/10.1145/3704884
  serial-number:
    doi: 10.1145/3704884
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 9
Download: stassen-2025-modelling.bib · stassen-2025-modelling.yml
Cited by (1)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory giovannini_ding_new_2025POPL · 2025

Gradually typed programming languages, which allow for soundly mixing static and dynamically typed programming styles, present a strong challenge for metatheorists. Even the simplest sound gradually typed languages feature at least recursion and errors, with realistic languages featuring furthermore runtime allocation of memory locations and dynamic type tags. Further, the desired metatheoretic properties of gradually typed languages have become increasingly sophisticated: validity of type-based equational reasoning as well as the relational property known as graduality. Many recent works have tackled verifying these properties, but the resulting mathematical developments are highly repetitive and tedious, with few reusable theorems persisting across different developments.

In this work, we present a new denotational semantics for gradual typing developed using guarded domain theory. Guarded domain theory combines the generality of step-indexed logical relations for modeling advanced programming features with the modularity and reusability of denotational semantics. We demonstrate the feasibility of this approach with a model of a simple gradually typed lambda calculus and prove the validity of beta-eta equality and the graduality theorem for the denotational model. This model should provide the basis for a reusable mathematical theory of gradually typed program semantics. Finally, we have mechanized most of the core theorems of our development in Guarded Cubical Agda, a recent extension of Agda with support for the guarded recursive constructions we use.

PDF · DOI · pldb
Cites 45 works (8 here)
With notes (8)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory giovannini_ding_new_2025POPL · 2025

Gradually typed programming languages, which allow for soundly mixing static and dynamically typed programming styles, present a strong challenge for metatheorists. Even the simplest sound gradually typed languages feature at least recursion and errors, with realistic languages featuring furthermore runtime allocation of memory locations and dynamic type tags. Further, the desired metatheoretic properties of gradually typed languages have become increasingly sophisticated: validity of type-based equational reasoning as well as the relational property known as graduality. Many recent works have tackled verifying these properties, but the resulting mathematical developments are highly repetitive and tedious, with few reusable theorems persisting across different developments.

In this work, we present a new denotational semantics for gradual typing developed using guarded domain theory. Guarded domain theory combines the generality of step-indexed logical relations for modeling advanced programming features with the modularity and reusability of denotational semantics. We demonstrate the feasibility of this approach with a model of a simple gradually typed lambda calculus and prove the validity of beta-eta equality and the graduality theorem for the denotational model. This model should provide the basis for a reusable mathematical theory of gradually typed program semantics. Finally, we have mechanized most of the core theorems of our development in Guarded Cubical Agda, a recent extension of Agda with support for the guarded recursive constructions we use.

PDF · DOI · pldb

Modular Denotational Semantics for Effects with Guarded Interaction Trees frumin-2024-modularPOPL · 2024
We present guarded interaction trees — a structure and a fully formalized framework for representing higherorder computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.
PDF · DOI · arXiv · pldb

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics sterling-2024-towardsCSL · 2024
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap - a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.
DOI · arXiv

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types VezzosiMortbergAbel2019ICFP · 2019
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
PDF · DOI · pldb

A domain theory for statistical probabilistic programming vakar-2019-aPOPL · 2019
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on ‘quasi-Borel predomains’. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory.
PDF · DOI · pldb

A convenient category for higher-order probability theory heunen-2017-aLICS · 2017
DOI · arXiv

Productive coprogramming with guarded recursion atkey-2013-productiveICFP · 2013
PDF · DOI · pldb

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013
Web · arXiv
External (37)
stassen-2025-modelling reference entries/refs/stassen-2025-modelling/stassen-2025-modelling.hel