Recent Seminars and Events at RIMS CS Group
This is a list of recent seminars and events hosted by our group.For the abstract of a talk, click its title.
2026
-
Ulrich Berger (Swansea University/Kyoto University)
23 April 2026, 11.00-Foundations and Applications of Program Extraction
In 1945, Kleene introduced an interpretation of arithmetic that assigns to a formula a set of numbers?called "realizers"?representing the formula's "computational content", rather than a simple truth value. He proved a "Soundness Theorem" establishing that every formula provable in intuitionistic arithmetic (Peano Arithmetic without the law of excluded middle) possesses a realizer.
Kleene’s realizability can be seen as a technically precise rendering of the central idea of constructive mathematics: that a proof of an object’s existence should contain a construction of that object. This principle is foundational to the Brouwer-Heyting-Kolmogorov (BHK) interpretation and the Curry-Howard correspondence. Program extraction, which is based on realizability, takes a formal proof (in a suitable constructive logic) and extracts a program that algorithmically solves the computational problems expressed by the proven formula.
In this talk, I will sketch the main developments in program extraction, highlighting some of the results obtained through the collaboration between Kyoto University and Swansea University within the framework of the EU project CCC (Continuity, Computability, Constructivity). I will also outline my research aims for my current four-month visiting professorship at Kyoto University.
-
Mirai Ikebuchi (Graduate School of Informatics, Kyoto University)
16 April 2026, 11.00-Anick Resolution for Lawvere Theories from Algebraic Discrete Morse Theory
Inspired by Brown's collapsing method (or discrete Morse theory) to obtain a free resolution of Z over the monoid ring ZM, we apply algebraic discrete Morse theory to compute the homology groups of Lawvere theories, which is defined as Tor of a certain module. We reinterpret known partial free resolutions arising from complete term rewriting systems in terms of collapsing of the normalized bar resolution. This perspective yields homological inequalities that bound the number of equational axioms in presentations and recovers classical results, such as lower bounds for group axiomatizations. Our main contribution is to extend these resolutions to higher dimensions.
-
Marcello Lanfranchi (Macquarie University)
9 April 2026, 11:00-Ehresmann connections in tangent categories
One of the fundamental concepts of differential geometry is the notion of connections. Connections are not only central to geometry, but they are also of fundamental importance in modern mathematical physics. Introduced by Rosicky and generalized by Cockett and Cruttwell, tangent categories offer a categorical context for differential geometry. In the last decade, there has been a lot of effort to internalize geometric constructions in tangent categories, to develop a unifying categorical language for geometry. As part of this program, in this talk, we extend Ehresmann connections to the tangent-categorical context.
This is work in progress and joint work with Geoff Cruttwell.
-
Symposium on Differentiation in Category Theory and Program Semantics
6-8 April 2026 (RIMS symposium at the RIMS main building) -
JS Lemay (Macquarie University)
2 April 2026, 11:00-On Hassei's Question about Traced Monoidal Closed Categories and Idempotent Comonads on Compact Closed Categories
In Hassei's paper “On Traced Monoidal Closed Categories”, he showed that a traced monoidal category was closed if and only if the canonical functor into the its INT construction has a right adjoint. As a consequence, every traced monoidal closed category is a reflexive subcategory of a compact closed category. As such, for a traced monoidal closed category, there is an idempotent comonad on its INT construction. Hassei pondered an open question of if there was a possible adjunction between traced monoidal closed categories and compact closed categories with a suitable notion of idempotent comonad. In this talk, I will review the main results of Hassei’s paper and investigate this open question (hopefully giving a correct answer to Hassei’s question).
2025
-
Rose Kudzman-Blais (RIMS)
18 December 2025, 11:00-An introduction to linear bicategories
Linearly distributive categories (LDC) were introduced by Cockett and Seely in 1992 as alternative categorical semantics for multiplicative linear logic to Barr’s *-autonomous categories, which make tensor and par primitive. In essence, LDCs are categories equipped with a tensor and a par monoidal structures, linked by linear distributivity transformations. *-autonomous categories are then recovered by introducing negation to LDCs via the notion of complementation. LDCs can be used to model variants of non-commutative linear logic, in particular by considering non-symmetric tensor and par products. However, non-commutative logical connectives are in some sense most naturally modelled by bicategorical composition. It is with this perspective in mind that, in 2000, Cockett, Koslowski and Seely introduced linear bicategories, the bicategorical analogue of LDCs. The prototypical example is the locally postal bicategory Rel of sets and relations, with standard composition modelling tensor and its deMorgan dual via complement-converse modelling par. In this talk, I will give an overview of the theory of linear bicategories: the definition, some relevant examples, how to consider negation in the bicategorical context, as well as the recent research on the topic.
-
Sangwoo Kim (Univ. of Tokyo)
11 December 2025, 11:00-Categorical Semantics of Regular Expressions on Categories of Weighted Binary Relations
The category Rel^M, defined by introducing a weighting by a monoid M to binary relations, is a generalization of Rel, the category of binary relations. Rel^M inherits many of the good structures present in Rel, such as products, coproducts, their coherence properties, and a total trace structure. In particular, it has been shown that Rel^M weighted by the monoid M=List Σ, consisting of strings and their concatenation operation, provides a categorical semantics for regular expressions. Furthermore, we found that representing this structure using string diagrams yields a geometrical interpretation of regular expressions. This discovery naturally allows for the definition of what we appropriately term "typed regular expressions".
In this talk, we will report on this definition and introduce ongoing research, such as the translation of known results from existing formal language theory.
-
Keisuke Hoshino (RIMS)
4 December 2025, 11:00-When operads are theories?
A planar operad may be thought as a (single-sorted) theory whose substitutions of terms have types that are depicted as planar trees. In other words, in a planar operad, terms can only be substituted along their (planar) “shape-trees”, which are determined by the *arities* equipped on the terms. These arities are genuinely pieces of *structure* rather than mere *properties*, in the following sense: although an equivalence of planar operads (respecting the arity data) always induces an equivalence of the corresponding theories (i.e. categories of algebras over `Set`), the converse implication fails in general (see [Leinster, Are operads algebraic theories?, 2004]).
Here the “shape trees” have unique nodes and a unique `n`-ary operation for each `n`, so such trees can be identified with natural numbers equipped with ordinary addition. This is the core part of the structure of the free monoid monad `fm`, and in this sense a planar operad can be regarded as a “monoid relative to the free monoid monad”. This picture relativises to any monad `T` on a category with finite limits: we can speak of “monoids relative to `T`”, usually called *`T`-operads*. A `T`-operad can then be thought of as a theory whose arities are taken in `T`.
Besides `fm` there is the free category monad `fc` on the category of (directed) graphs, and an `fc`-operad is precisely a virtual double category whose loose graph is the terminal graph. Although `fm` and `fc` are very similar and share many features (for instance *familial representability*), `fc`-operads are significantly better behaved than `fm`-operads: their arities really are *properties*. In particular, once one has shown that the relevant arities exist, one can safely forget them and regard an `fc`-operad simply as a theory over the category of graphs.
In this talk I will give a sufficient condition on a monad `T` for its `T`-operads to have this “arity-as-property” behaviour, and I will discuss how this condition relates to gauntness and (strong) connectedness. This is a fairly new idea and still not completely organised; parts of it are already used in my PhD thesis.
-
Masahito Hasegawa (RIMS)
27 November 2025, 11:00-Reflexive racks
We outline part of our (still ongoing) attempts to relate semantics and low-dimensional topology.
A rack is a set equipped with a self-distributive binary operator which is bijective on the left argument. It is well known that racks provide invariants of (framed) tangles. In particular, quandles, aka idempotent racks, are frequently used for obtaining invariants of knots.
In this talk, we introduce reflexive racks, which are racks with an additional binary operator that satisfies certain conditions. Just like racks give invariants of framed tangles, reflexive racks give invariants of braided lambda terms (and more generally braided lambda-graphs) modulo the beta-equality.
We show that a reflexive rack gives rise to a (non-extensional) braided combinatory algebra, which in turn induces a braided monoidal category with a reflexive object (hence the name "reflexive rack") via the internal PROB construction.
It turns out that every rack is a sub-rack of a reflexive rack. Interestingly, a reflexive quandle is necessarily trivial (in an appropriate sense), so it is essential to use racks rather than quandles.
We also explain how a reflexive rack can be seen as a type assignment system for the braided lambda calculus.
-
JS Lemay (Macquarie University)
6 November 2025, 11:00-Free Differential Modalities
In the categorical semantics of linear logic, the exponential is characterized by coalgebra modalities, while for the differential linear logic, the exponential is formalized by differential modalities. In this talk, I will explain how using algebraically free commutative monoids, we can build free differential modalities on coalgebra modalities. This is joint work with Richard Garner, based on our recent paper: arXiv:2508.14320 .
-
Zeinab Galal (RIMS)
31 July 2025, 11:00-A categorical viewpoint on systems of fixpoint equations
Fixpoints play an important role in both denotational semantics where they are used to represent recursively defined programs and data types as well as in operational semantics where many behavioral equivalences are obtained as fixpoints of some relation transformers.
In the categorical theory of fixpoint operators, we usually consider one fixpoint operator at a time and little attention is given to the study of mixed fixpoint operators where we take a different fixpoint operator for each variable. Systems combining least and greatest fixpoints over lattices are an important example as they are the basis of many static analysis and model checking methods.
I will present in this talk an axiomatization of mixed fixpoint operators first in the 1-categorical setting and then extend to 2-categories. The 2-dimensional framework allows to capture the examples of (parametrized) initial algebras and coalgebras of accessible functors, analytic and polynomial functors.
-
Kazushige Terui (RIMS)
3 July 2025, 11:00-On bridge theorems in abstract algebraic logic
A typical subject in abstract algebraic logic is the correspondence between properties of propositional logics and those of the associated classes of algebras, known as bridge theorems. Let L be an algebraizable logic (in the sense of Blok and Pigozzi) whose equivalent semantics is a quasivaraiety K. For instance, L may be the intuitionistic propositional calculus and K be the variety of Heyting algebras.
On the logical side, one asks whether L satisfies (i) the local deduction property, (ii) the Robinson property and (iii) the strong deductive interpolation property. On the algebraic side, one asks whether K satisfies (1) the relative congruence extension property, (2) the amalgamation property and (3) the transferable injection property. As is well known, we have bridge theorems (i)<->(1), (ii)<->(2) and (iii)<->(3). We also have (i)+(ii)=(iii) and (1)+(2)=(3).
While each fact is well understood, we have not yet reached a crystal-clear understanding of the overall picture. To obtain a more systematic account, we work on the category Th(L) of L-theories and try to express the logical properties (i), (ii) and (iii) therein. Once this has been achieved, the bridge theorems boil down to the obvious categorical equivalence between Th(L) and K. This also allows us to understand the two facts (i)+(ii)=(iii) and (1)+(2)=(3) in a completely parallel way.
-
Mirai Ikebuchi (Graduate School of Informatics, Kyoto University)
5 June 2025, 11:00-Cohomology of small cartesian closed categories
(Co)homology of an mathematical object is an important invariant of the object. Cohomology theories are defined for various mathematical objects in various ways, but Quillen (1967) proposed a unified way to define a cohomology of an object of a general algebraic category with simplicial methods. In this talk, we consider Quillen cohomology of small cartesian closed categories and show that it is isomorphic to Hochschild cohomology, another famous cohomology theory. This is an extension of the isomorphism for small categories by Dwyer&Kan (1988), and that for Lawvere theories by Jibladze&Pirashvili (2006).
The talk will begin by explaining that (co)homology of small cartesian closed categories can be effectively applied to study higher-order equational theories, i.e., theories of equations between lambda-terms with unit, product, and function types.
-
Hayato Nasu (RIMS)
29 May 2025, 11:00-Double categories of relations relative to factorization systems and fibrations/ Exploring double categories of relations
I will deliver two distinct 20-minute talks in this session as rehearsals for presentations at workshops.
1. The applications of (virtual) double categories have expanded in recent years. In this talk, we explore double categories of relations at varying levels of generality. We begin with the double category of sets, functions, and relations; we will also generalize it, first using factorization systems and then using (Grothendieck) fibrations. This talk is partly based on joint work with Keisuke Hoshino (Kyoto Univ) as well as my master's thesis.
2. Bicategories of relations or spans have attracted many category theorists since the 1970s, and the study has been extended to the world of double categories in recent years. In this talk, I will provide an overview of the development of this field, particularly in relation to a condition called the Frobenius axiom, as presented in Walters and Wood's paper "Frobenius objects in Cartesian bicategories." This axiom can be understood as a criterion for a double category to qualify as a "double category of relations," and I will explain some results that support this idea.
-
Nicola Di Vittorio (Macquarie University)
3 April 2025, 11:00-2-derivators: two different takes
Derivators were introduced by Grothendieck and Heller to formalize homotopy theory, axiomatising what happens when we work with collections of homotopy categories of diagrams inside a model category.
Model categories, in turn, can be seen as a presentation of (∞, 1)-categories, a concept described using various models. With a shift of perspective, Riehl and Verity realized that (∞, 1)-categories can be treated as a primitive concept within their theory of ∞-cosmoi. In this context, the theory of (∞, 1)-categories can be developed without ever having to define them explicitly. Some deep results ensure that much of the theory of an ∞-cosmos can be developed inside a quotient, its homotopy 2-category.
During my PhD, I have introduced an higher-dimensional version of the theory of derivators, designed to capture key properties of the ∞-cosmological approach to (∞, 1)-category theory. In this talk, I will discuss this theory in two different variants: one using 2-categories and a more recent one using simplicial categories.
-
Kengo Hirata (University of Edinburgh / Kyoto University)
25 February 2025, 11:00-Towards a higher-order quantum programming language with quantum control
In contrast to a classical bit, which can only take the value of either 0 or 1, its quantum counterpart can take a state of a superposition of 0 and 1, and the capability of superposition is expected to make quantum computation more efficient than classical computation. The superposition of 0 and 1 in a qubit is a superposition of data, and it is natural to wonder if it is possible to superimpose not only data but also programs. For example, a particular superposition of programs, called quantum SWITCH, has attracted much attention, and its implementation and computational advantages have been studied mainly in the physics community. However, most of the existing programming languages with quantum control mechanisms usually restrict the target of quantum control to be first-order program that applies unitary gates to qubits, and such languages cannot express the quantum SWITCH. In this talk, I describe two challenges in extending a language to support more flexible quantum control and discuss a solution with typing rules based on linear logic.
-
Kyoto Category Theory Meeting
12 February 2025
2024
-
Pierre-Marie Pedrot (INRIA)
2 December 2024, 14:00-“Upon This Quote I Will Build My Church Thesis”
The internal Church thesis (CT) is a logical principle stating that any function f : N → N is computed by a concrete program in some Turing-complete language. CT has been widely used in constructive mathematics, most specifically in the Russian tradition. On the other side of the iron curtain, Martin-Lof Type Theory (MLTT) was designed as the modern embodiment of Bishop-style neutral mathematics. It should come as a surprise that the natural type-theoretic equivalent of CT was conjectured to be inconsistent with MLTT. In this talk, we will prove that this conjecture is false, by introducing “MLTT”, a consistent extension of MLTT with quoting primitives that implements CT in a computational way.
-
Richard Garner (Macquarie University)
15 November 2024, 11:00-Bisimulation versus trace equivalence
A labelled transition system with label-set B comprises a set of states S together with an operation which to each state from S, non-deterministically assigns an output symbol in B and a new state in S. A probabilistic generative system is the same thing, except that the non-deterministic assignment above becomes a probabilistic one.
For labelled transition systems and probabilistic generative systems, there are many different meaningful notions of equivalence between states; the extremal choices are bisimulation equivalence and trace equivalence. It is well known that two states of a system are bisimilar if they become the same under the unique map to the final such system. On the other hand, a line of research, started by Power?Turi, and developed further by Hasuo, Jacobs and Sokolova, characterises trace equivalence in terms of equality under the unique map to a terminal object in a suitable Kleisli category.
We propose a refinement of the Power?Turi?Hasuo?Jacobs?Sokolova theory, which instead characterises trace equivalence in terms of a terminal object in a suitable category of Eilenberg?Moore algebras. For the examples listed above, this recovers the full infinitary trace given by closed sets of B^N (for labelled transition systems) and probability distributions on B^N (for probabilistic generative systems).
(joint work with Soichiro Fujii)
-
Workshop on Categorical Structures and Computer Science (CSCS2024)
31 October and 1 November 2024 -
Fabio Zanasi (University College London)
21 August 2024, 11:00-Graphical Quadratic Algebra ? A Complete Diagrammatic Calculus of Gaussian Processes and Least-Squares Problems
Least-square problems lie at the core of statistical modelling. Their mathematical theory is of independent interest, as it reveals a web of connections between linear algebraic methods and Gaussian probability.
In this talk, we present a structured approach to least-square problems, which uses categorical algebra to develop a compositional perspective on these systems. In particular, we introduce Graphical Quadratic Algebra: a sound and complete axiomatic calculus for least-squares problems. The name “Quadratic” comes from quadratic relations, which we identify as the semantic domain in which least-square problems may be studied compositionally. The name “Graphical” is due to the way we present our calculus, using the graphical formalism of string diagrams. String diagrams offer a user-friendly interface for algebraic manipulations, while maintaining the fully formal status of a syntactic object.
Our investigation sheds light on the relationship between least-square problems, Gaussian probability, and linear algebra, as we show that fragments of Graphical Quadratic Algebra axiomatise categories of linear algebraic and Gaussian processes. Furthermore, we will showcase our approach on three case studies: (1) Ordinary Least Squares regression, (2) probabilistic programming with uninformative priors, (3) noisy electrical circuits.
-
Soichiro Fujii (ex-visiting fellow at Macquarie University)
15 August 2024, 11:00-Enrichment and families over a virtual double category
Enriched category theory gives rise to a 2-functor Enr from a suitable 2-category of enrichment bases to the 2-category 2-CAT of 2-categories, sending each base V to the 2-category Enr(V) = V-Cat of V-categories. Classically, the monoidal categories are taken as the enrichment bases, but there have been several extensions. In this talk, I will show that the 2-functor Enr becomes a parametric right 2-adjoint if we take the virtual double categories as the enrichment bases, by decomposing the 2-functor Enr_1 : VDBL --> 2-CAT/Enr(1) into a few basic right adjoint 2-functors. The powerfulness (or exponentiability) of discrete opfibrations between virtual double categories and the notion of horizontal unit in a virtual double category play essential roles.
(Joint work with Steve Lack)
-
Nick Hu (University of Oxford)
8 August 2024, 11:00-Coherent invertibility in associative n-categories
In this talk, I will present my PhD work on enhancing the combinatorial foundation of the proof assistant homotopy.io to support invertible generators.
The theory of associative n-categories has been employed to give a combinatorial model of directed higher categories amenable to computer implementation, presented as n-dimensional string diagrams. However, the theory lacks a notion of inverse, which would require the existence of cancellation moves along with an infinite collection of higher-dimensional coherence data.
We generalise the theory to support invertibility by equipping generators with framing data, allowing for a natural representation of the inverse. Using this framed zigzags approach, we show that the required cancellation moves and coherence data arise uniformly via a colimit mechanism. We use tools from enriched category theory to justify correctness of our constructions, and exhibit a proof assistant which implements our theory.
-
Vincent Moreau
(IRIF & Universite Paris Cite & Inria Paris)
25 July 2024, 11:00-Profinite lambda-terms: when Stone spaces meet cartesian closed categories
Profinite words provide a way to speak about the limiting behavior of words with respect to finite monoids. They assemble into a topological monoid, defined categorically by codensity, which is the Stone dual of the Boolean algebra of regular languages of words and is thus a central object of automata theory.
The Church encoding of finite words into the simply typed lambda-calculus, i.e. the language of cartesian closed categories, has been used by Salvati to introduce a higher order notion of regular language. In this work, we formulate in a clean and principled way a notion of profinite lambda-term, whose space is the Stone dual of Salvati's regular languages, and which live in harmony the principles of Reynolds parametricity. We show that profinite lambda-terms generalize the notion of profinite word to the higher order and are compositional as they assemble into a cartesian closed category.
-
Mayuko Kori (NII)
18 July 2024, 11:00-Composing Codensity Bisimulations
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system.
In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality.
In addition, we propose a compositional variant of Komorida et al.'s codensity games for bisimilarities. A novel feature of this variant is that it can also compose game invariants, which are subsets of winning positions. Under our sufficient condition of the liftability of distributive laws, composed games give an alternative proof of the preservation of bisimilarities under the composition.
(Joint work with Kazuki Watanabe, Jurriaan Rot, and Shin-ya Katsumata)
-
Susumu Nishimura (Dept. Math, Kyoto University)
11 July 2024, 11:00-Checking Consistency of Distributed Programs via Grobner Bases over Boolean Polynomial Ring
The celebrated Asynchronous Computability Theorem of Herlihy and Shavit characterizes the class of computable distributed tasks by the composition of two topological maps over simplicial complexes: the standard chromatic subdivision and a decision map.
I will propose a simple functional-style programming language for writing distributed programs, where the topological maps are defined by pattern matching over algebraic data types and ordered set partitions, which index simplexes and their subdivisions, respectively. The topological maps must be verified to maintain a certain topological consistency: A vertex shared by two input simplexes are mapped to the same output vertex. I developed a method that checks this consistency by generating a constraint from the given definition and then solving it using Grobner bases over Boolean polynomial ring [Sato et al. 2011; Inoue 2012].
I will also give a demonstration of a prototype implementation.
-
Satoshi Nakata (RIMS)
27 July 2024, 11:00-Prenex normal form theorems in intuitionistic arithmetic and the effective topos
The fact that every first-order formula has a prenex normal form in classical logic is known as the prenex normal form theorem, recognized as one of the most widely used theorems in mathematical logic. However, this theorem does not generally hold for intuitionistic theories. Specifically, Fujiwara and Kurahashi have identified the proof-theoretic strength of certain variants of prenex normal form theorems among semi-classical arithmetic, such as Γ-DNE for some class Γ of formulas. Among their findings, they provided negative evidence: the prenex normal form theorem for Σ1 does not hold in HA+Σ1-DNE.
In this talk, I will present an alternative proof of this negative result based on topos-theoretic arguments.
This talk is a rehearsal for my presentation at TACL.
-
Masahito Hasegawa (RIMS)
6 June 2024, 11:00-Braids, twists, trace and duality in combinatory algebras
We investigate a class of combinatory algebras, called ribbon combinatory algebras, in which we can interpret both the braided untyped linear lambda calculus and framed oriented tangles. Any reflexive object in a ribbon category gives rise to a ribbon combinatory algebra. Conversely, from a ribbon combinatory algebra, we can construct a ribbon category with a reflexive object, from which the combinatory algebra can be recovered. To show this, and also to give the equational characterisation of ribbon combinatory algebras, we make use of the internal PRO construction developed in our recent work. Interestingly, we can characterise ribbon combinatory algebras in two different ways: as balanced combinatory algebras with a trace combinator, and as balanced combinatory algebras with duality.
This is a joint work with Serge Lechenne (to be presented at LICS2024).
-
Bakh Khoussainov (UESTC, China and The University of Auckland, New Zealand)
8 February 2024, 11:00-Probability structures
We develop a framework for reasoning about statistical properties in relational structures. To achieve this, we introduce smooth probability structures defined as relational structures equipped with a sequence of probability distributions.
We design a language, termed LSPS, which is dedicated to reasoning about statistical properties in relational structures. Given a smooth probability structure, with each formula $\phi(\bar{x})$ in the LSPS language we associate a family of probability spaces that encapsulate the statistical information about all tuples that satisfy $\phi$. This fusion of connecting relational structures and statistics is a novel concept. We study the questions of axiomatizability, decidability, and undecidability of valid LSPS formulas. Finally, if time permits, we initiate the investigation of algorithmic questions suited for smooth probability structures.