In recent years, there has been much work done in probabilistic semantics. Most of them fall in one of two categories; those based on monads and those based on linear logic. At the semantic level, these two different semantics correspond to distinct basic programming abstractions. In this case, semantically, programming with monads corresponds to programming with Markov kernels, while linear logic corresponds to programming with linear operators.

In this talk I will go over recent work of mine that tries to establish a formal connection between these two families of semantics. I will start by presenting a new core calculus for programming with Markov kernels and linear operators, will show that this formalism encompasses useful models from the probabilistic semantics literature and will conclude by sketching some applications of this formalism to the new research program of synthetic probability theory.

In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements. We show that inductive data types and recursion can also be effectively modelled in this setting. However, these results do not straightforwardly extend to the pure quantum case. We provide insights into the challenges encountered and propose potential directions for addressing these limitations, for example with guarded recursion.

(Self) references: Classical reversible semantics: https://doi.org/10.4230/LIPIcs.FSCD.2024.19 / https://arxiv.org/abs/2309.12151 First-order quantum semantics (chapter 3): https://theses.hal.science/tel-04625771 / https://arxiv.org/abs/2406.07216 Non-cartesian guarded recursion: https://arxiv.org/abs/2409.14591

Like time in physics, computations can be reversible: the inverse of a deterministic computation is itself a valid computation, provided the program's state retains sufficient information to allow rollback. However, reversing a computation in distributed systems presents a challenge due to non-determinism. The inversion process must respect causality to maintain consistency. Syntactically, reversing a concurrent program requires tracking computation events in a way that preserves information during reductions, despite the absence of a global scheduler. From a denotational perspective, traditional models interpret concurrent programs as partial orders of configurations, where configurations consist of sets of computation events. Executing a computation involves removing the corresponding events from all configurations using set difference, while discarding incompatible configurations. In this talk, we introduce a generalization of these traditional models to accommodate reversibility, employing symmetric difference. This approach interprets reversible computation as a partial group action on sets of configurations.

The Ahlbrandt-Ziegler result in model theory asserts that a countably categorical theory is characterised, up to bi-interpretability, by the topological automorphism group of its (unique) countable model, thus permitting a study of these theories by group-theoretic properties.

Removing the countable categoricity assumption necessitates using topological groupoids rather than groups. We will describe a groupoidal generalisation of the Ahlbrandt-Ziegler result using topos theory.

Our result extends the results in the topos-theoretic literature of Awodey, Butz, Caramello, Forssell and Moerdijk, while being orthogonal to the parallel generalisation of Ben Yaacov.

Summary: The starting point of this talk is the structure of the object $!Bool$ in probabilistic coherent spaces. For the purpose of building a semantics interpretation for PCF_proba, it is enough to consider elements of $!Bool$ that are promotions of elements in Bool, but $!Bool$ contains also more exotic elements, that can nonetheless be seen as probabilistic samplers (in the sense that they can handle any number of query from a program !Bool → sigma to its argument, seen as a random oracle). In this work, we present a caracterisation of all total elements in !Bool: we show that they can all be seen as *continuous mixture* of promotions. The central element of this proof is an extension to the category of integrable cones of the categorical version[1] of the De Finetti theorem (that says that there is a one-to-one correspondance between the continuous probability distributions on [0,1], and the infinite exchangeable sequence of discrete random variables on booleans).

[1] B. Jacobs and S. Staton. De finetti’s construction as a categorical limit, CMCS 2020.

Storage modalities provide the categorical interpretation of the exponential modality from Linear Logic, while differential storage modalities do the same in Differential Linear Logic. Briefly, a storage modality is a special kind of comonad, while a differential storage modality is a storage modality equipped with a deriving transformation (equivalent a codereclition). In this talk, I’ll explain how using Kelly's notion of algebraically-free commutative monoids, we can construct free differential storage modalities over storage modalities. When taking the initial storage modality, we get the initial differential storage modality which is related to the Faà di Bruno construction and also recaptures the exponential modality in Clift and Murfet's Differential Linear Logic model. This is joint work with Richard Garner.

The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

Joint work with Hagit Attiya and Armando Castañeda.

Lawvere’s (hyper-)doctrines are a categorical tool that allows the analysis of both the syntax and the semantics of logical theories using the same mathematical structure. In this talk, we explore a possible interpretation of Henkin’s Theorem for first-order logic (“Every consistent theory has a model”) via bounded implicational existential doctrines. To achieve this goal, at first we study the meaning in the framework of doctrines of “adding a constant to a language” and “adding an axiom to a theory”. Then, starting from a consistent doctrine, we use these construction to build a rich doctrine - in which every valid formula of the kind ∃xφ(x) there exists a witness constant c such that φ© holds. Finally, we show that a rich doctrine admits a model, i.e. a morphism towards the subset doctrine. Henkin’s Theorem for doctrines follows from these results, and our proof is modelled on the main lines of the original one.

We will present a very general syntax that aims to export tools and techniques found in linear logic (intersection types, Taylor and Böhm approximations, geometry of interaction…) in a systematic way in other languages or calculus. That being still a work in progress, details will be given in a restriction of this syntax, in which we present an axiomatic definition of “approximation system”, based on a notion of fibration, aiming to capture this phenomenon as generally as possible. In this talk, we will explore the immediate consequences of the definition, introduce several concrete instances of it, and obtain well-known theorems as direct applications of the general framework.