π-calculus, Session Types research at the University of Oxford
We propose a framework of universal algebra for specifying graded monads on the category of pseudometric spaces and nonexpansive maps with grades in the additive preordered monoid of extended positive reals. The ensuing concept of graded quantitative theory combines ideas from the work on universal algebra over relational Horn models and the graded algebraic theories of Kura. Our key motivation is to develop a presentation of the so-called neighborhood monad that features in the denotational semantics of Numerical Fuzz, a linear type system for tracking bounds on the rounding error incurred in numerical programs. In this direction, we introduce the graded quantitative theory of neighbors and prove that its associated variety admits free algebras, which enables us to associate a graded monad with the theory. We leave it open for future work to establish the precise relation between the neighborhood monad and our graded quantitative theory of neighbors.
@inproceedings{FFFGHR2025, author = {Max Fan and Chase Ford and Jonas Forster and Jón Hákon Garðarsson and Justin Hsu and Jessica Richards}, title = {{Towards an Axiomatisation of the Neighborhood Monad}}, booktitle = {1st International Workshop on Behavioural Metrics and Quantitative Logics, Aarhus, Denmark}, pages = {--}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{"{u}}r Informatik}, year = 2025 }
@inproceedings{FFFGHR2025, author = {Max Fan and Chase Ford and Jonas Forster and Jón Hákon Garðarsson and Justin Hsu and Jessica Richards}, title = {{Towards an Axiomatisation of the Neighborhood Monad}}, booktitle = {1st International Workshop on Behavioural Metrics and Quantitative Logics, Aarhus, Denmark}, pages = {--}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{"{u}}r Informatik}, year = 2025 }