Semantics Tuesday March 18, 2025, 3PM, Salle 3071 Vladimir Zamdzhiev (LMF, Inria Saclay) Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory In this talk we recall how quantum operations (also known as channels) are modelled mathematically in both the Heisenberg and Schrödinger pictures of quantum theory. The two pictures are dual to each other and we recall how the theory of operator spaces can be used to describe this duality in mathematical terms. Operator spaces, studied in noncommutative geometry, are the noncommutative (or quantum) analogue of Banach spaces. We prove that the category OS (operator spaces with complete contractions as morphisms) is locally countably presentable and a model of Intuitionistic Linear Logic in the sense of Lafont. We then describe a model of Classical Linear Logic, based on OS, whose duality is compatible with the Heisenberg-Schrödinger duality of quantum theory. In the later model, the mathematical descriptions of systems in the Heisenberg picture correspond to formulas with negative logical polarity, whereas those in the Schrödinger picture correspond to formulas with positive logical polarity. Time permitting, we can also cover other interesting features of the model(s). Joint work with Bert Lindenhovius. Semantics Wednesday March 12, 2025, 10:45AM, Salle 3071 Elena Di Lavore (Oxford) Effectful streams for dataflow programming Effectful streams give formal compositional coinductive semantics to effectful synchronous dataflow programs. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimilarity implies effectful trace equivalence. This talk is based on joint work with Giovanni de Felice and Mario Román, and on more recent joint work with Filippo Bonchi and Mario Román. Semantics Tuesday February 25, 2025, 3PM, Salle 3071 Ariadne Si Suo (Cambridge) Type Checking is Proof Reductions in Classical Linear Logic I will try to convince you type checkers can be seen as logic programs with ‘directions’, and doing type checking correspond to proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, by writing bidirectional typing rules as directional logic programs. If time permits, I will tell you some categorical details, or possible extensions to accommodate more expressive type systems. Based on joint work with Vikraman Choudhury and Neel Krishnaswami. Semantics Tuesday February 18, 2025, 3PM, Salle 3071 Quentin Aristote Monotone weak distributive laws over the lifted powerset monad in categories of algebras Noticing the similarity between the monotone weak distributive laws combining two layers of non-determinism in sets and in compact Hausdorff spaces, we study whether the latter law can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras: we then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases. Semantics Wednesday February 12, 2025, 10:45AM, Salle 3071 Umberto Tarantino Arrow algebras, algebraic structures for modified realizability In this talk I will introduce arrow algebras, “algebraic” structures inducing toposes through Pitts' tripos-to-topos construction which generalise Alexandre Miquel’s implicative algebras, and I will present appropriate notions of morphisms between arrow algebras corresponding to morphisms of the associated triposes. The weakening of the axioms, from implicative algebras to arrow algebras, allows the latter to perfectly factor through the construction of realizability toposes starting from partial combinatory algebras; moreover, it allows for a particularly simple description of subtoposes of the induced toposes in terms of nuclei on the underlying arrow algebra, generalising the notion of nucleus on a frame. As an example of these properties, I will show how modified realizability can be lifted to the level of arrow algebras, recovering and extending some results known in the literature at the level of partial combinatory algebras. Semantics Tuesday February 4, 2025, 3PM, Salle 3071 Arturo De Faveri Clones, Boolean algebras, and hypervarieties A clone on a set is a family of finitary operations on the set that is closed under projections and composition. Abstract clones are the algebras for the many-sorted equational presentation that axiomatises this structure. Categorically, they are (finitary, one-sorted) algebraic theories. Inspired by works in algebraic logic, we shall define an equational class of abstract clones, tentatively dubbed “partition clones'', and describe some of their properties; in particular, we will show that this family of abstract clones has lot in common with Boolean algebras. Among the results we shall present, there is a theorem concerning the lattice of hypervarieties (i.e. varieties of abstract clones) already proven in 1991 by George M. Bergman from a different perspective. We shall explain the link between his approach and ours. Semantics Tuesday January 28, 2025, 3PM, Salle 3071 Rémi Di Guardia A simple proof of sequentialization for proof-nets, and links with graph theory Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyễn but focusing on edge-colored graphs instead of perfect matchings. [Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair] Semantics Tuesday January 7, 2025, 3PM, Salle 3071 Thomas Ehrhard Upper approximating probabilities of convergence of PCF programs, using extensional probabilistic coherence spaces Probabilistic coherence spaces (PCSs) provide an adequate, and actually fully abstract, denotational model of probabilistic PCF (an idealised Turing complete functional language extended with probabilistic choice). Given a closed probabilistic PCF term M of type bool for instance, PCSs provide therefore a way to approximate from below the probability p that M reduces, eg, to true. I will show how, extending PCSs with an “extensional structure”, it is also possible to approximate this probability p from above. These extensional PCSs form a model of LL, and are a probabilistic analog of Berry's bidomains. I will explain how this approximation mechanism can be straightforwardly implemented using a Krivine Machine which computes finite approximants of a powerseries associated with M by the extensional PCS semantics. If time permits, there will be a demo.