internal languages for probabilistic programming
Categorical semantics of probabilistic programming has traditionally been restricted to a few semantic universes: standard borel space via the Giry monad, quasiborel spaces for higher-order probability, or ωPAP spaces for differentiable probability theory. However, the synthetic approach to probability theory promises a more algebraic and general approach to program semantics, less focused on the particular analytic aspects of these models.
While the internal languages of complex categorical structures have moved large amounts of research effort — consider topos theory with its Mitchell-Bénabou language, or ∞-toposes via homotopy type theory — arguably, the internal languages of simpler and more general categorical structures (Markov categories, restriction categories, duoidal categories) have received considerably less attention.
The development of a probabilistic programming language with exact observations based on the internal language of traced distributive partial Markov categories.