Differentiation in category theory and program semantics

• 9:00-9:30: Morning Chat and Welcome

• 9:30-10:30: Jean-Simon Pacaud Lemay

Title: Tutorial 

Abstract: TBD

• 10:30-11:00: Morning Break 

• 11:00-11:30: Rose Kudzman-Blais

Title: Differential Linearly Distributive Categories

Abstract: The categorical semantics for linear logic, developed by Girard in 1987, are given by *-autonomous categories. The monoidal product models multiplicative conjunction (tensor) and the involutive functor models linear negation. Multiplicative disjunction (par) is then considered by taking the de Morgan dual. In 1992, Cockett and Seely introduced linearly distributive categories (LDC) to provide alternative semantics which take tensor and par as the primitive categorical structures. Through this lens, the relationship between tensor and par was promoted, axiomatized by linear distributivity.

Differential linear logic (DiLL) is an extension of linear logic developed by Ehrhard and Regnier in 2003, which adds rules to the exponential modalities encoding differentiation of proofs. In 2006, Blute, Cockett and Seely introduced differential categories as a categorical framework for DiLL and, more broadly, the basic theory of differentiation. Precisely, the semantics of DiLL can be given by an additive *-autonomous category with a monoidal coalgebra modality, modelling the exponential modality ! (bang/of course), equipped with a codereliction. While DiLL and differential categories have been studied in depth, there is generally little mention of the exponential modality ? (whimper/ why not), even though it is inherently present in the semantics. This mirrors the case of par and its relationship to tensor, which was under-represented in research prior to the introduction of LDCs. In this talk, I will be presenting an on-going project with Lemay which endeavours to fill the gap by developing differential linearly distributive categories. This project relies heavily on previous efforts by Blute, Cockett and Seely who axiomatized the semantics for the exponential modalities in the context of LDCs via storage, and linear functors and transformations. Moreover, this was initially motivated by recent work by Kerjean and Lemay which made explicit use of both exponential modalities in the context of differential categories. 

•  11:30-12:00: Jean-Baptiste Vienney

Title: Four variants of differential categories

Abstract: During my PhD studies, I’ve explored four variants of differential categories obtained by tweaking the classical definition (one of them in collaboration with JS Lemay). These variants are respectively called relative, graded, filtered and Hasse-Schmidt differential categories.

The goal of this talk is to briefly introduce each of them: what they are useful for, how they are defined and a few interesting examples. 

The relative version replaces the comonad in the definition of a differential category by the more flexible notion of a relative comonad. The graded and filtered versions add a notion of degree in the sense of polynomials to morphisms. Finally, the Hasse-Schmidt version refines the differential structure to handle Taylor expansions in categories lacking positive rational scalars.

I will also explain two theorems: one extracts a filtered differential category from a differential category and the other glues a filtered differential category into a differential category.

• 12:00-12:30: Ryuya Hora  

Title: A Rota-Baxter equation for winning games

Abstract: In 1901, Bouton proved a famous result on the winning strategy for Nim using binary xor ⊕︎. Once the theorem is stated, the only non-trivial part of its proof is the equation mex(S)⊕︎mex(T) = mex(mex(S)⊕︎T ∪ S⊕︎mex(T)), which is quite similar to the integral version of the Leibniz rule, known as the Rota-Baxter equation ∫f ×∫g = ∫((∫f) × g + f×∫g).

In my talk, I first discuss a categorical formulation of games as recursive coalgebras, based on my preprint (https://arxiv.org/abs/2510.22886). Then, I explain how the differential structure on the category of games gives rise to invariants valued in Rota-Baxter rigs, in particular, the Rota-Baxter rig consisting of finite subsets of ℕ and binary xor ⊕︎. This talk is partially based on an ongoing work with Ryo Suzuki.

• 12:30-14:00: Lunch Break 

• 14:00-14:30: Thomas Seiller

Title: Linear realisability, nuclei of enriched adjunctions, and textual corpora

Abstract: The impressive results obtained by generative language models witness that statistical information about a (large enough) corpus can be used to extract some structure of natural langage. As part of a general effort to investigate how to mathematically understand this process, Bradley, Gastaldi and Terilla have proposed a generalization of the standard notion of formal concepts to incorporate quantitative information. This approach consists in moving from sets to functions over sets (using presheaves): the generalized formal concepts are thus obtained as so-called nuclei (fixed points) of an adjunction. I will explain how this construction turns out to coincide with linear realisability, a technique to define models of (fragments of) linear logic. This leads to a dual structure on nuclei defined from textual corpora: a geometric structure, represented by a tropical cell complex, and a logical structure.

• 14:30-15:00: Holger Thies

Title: Spaces of Sequences in Computable Analysis and Applications to Differential Equations

Abstract: The category of represented spaces provides a convenient setting for computable analysis, where objects are sets equipped with representations assigning names from Baire space to their elements, and morphisms correspond to computable functions realized by algorithms operating on these names.  

We present recent results on the formalization of computable analysis in this framework and its implementation in the Rocq proof assistant, with a focus on applications to verified numerical computations. In particular, we consider spaces of summable sequences and their connection to convergent power series and holomorphic functions. These constructions allow us to formalize classical methods for solving analytic ordinary differential equations, leading to a verified solver for systems of multivariate analytic ODEs in Rocq.

• 15:00-15:30: Afternoon Break 

• 15:30-16:00: Aymeric Walch

Title: Web models of Linear Logic and their differential structure

Abstract: We provide in this talk a generic construction of web models of Linear Logic based on a partial sum operation. Different choice for this sum operator encode different computational properties of programs, ranging from determinism to randomness, finite non-determinism, and arbitrary non determinism. In particular, our construction captures in a unified setting a wide array of web models of Linear Logic : the (weighted) relational model, (probabilistic) coherence spaces, finiteness spaces and Köthe spaces.

We then describes differentiation and Taylor expansion in these web models. To that end, we generalize the theory of differential categories – which are enriched over monoids – to a theory of differentiation in categories enriched over partial sums. This “coherent” theory of differentiation and of Taylor expansion suggests the existence of a purely deterministic (or probabilistic) resource calculus.

• 16:00-16:30: Soichiro Fujii

Title: Virtual double categorical construction of a 2-dimensional model of differential linear logic

Abstract: The 2-monad on Cat for symmetric monoidal categories extends to the bicategory Prof of profunctors, giving rise to a linear exponential pseudocomonad. This has been used to give a 2-dimensional model of differential linear logic. In this talk, I will describe a construction of this pseudocomonad and its variants using virtual double categories. This talk is based on discussions with Keisuke Hoshino.

• 9:00-10:00: Shin-Ya Katsumata

Title: Differentiable Causal Computations via Delayed Trace

Abstract: A recurrent neural network (RNN) is an extension of neural networks designed to process time-series data and has a structure similar to a Mealy machine. In this study, we present a method for extending the differentiation operation - essential for tuning neural network parameters - to RNNs. This differentiation operation satisfies the axioms of differential categories formulated by Cockett and others, and we also show that differentiating an RNN and then taking a finite unrolling yields the same result as the operation known as Backpropagation Through Time (BPTT), where the RNN is first unrolled finitely and then differentiated.

• 10:00-11:00: Morning Break 

• 11:00-11:30: Takahiro Sanada

Title: A programming language and its semantics for practical neural networks

Abstract: We present a programming language to implement neural networks. The language has algebraic effects and a novel handlers, called reverse handlers, for arrows. The semantics of  the language is given by promonads on reverse differential restriction categories. Using reverse handlers, we can separate abstract design of neural networks and their implementation. This work is based on our preprint https://arxiv.org/pdf/2602.18090, and is joint work with Keisuke Hoshino, Kenshin Hirai and Shin-ya Katsumata.

•  11:30-12:00: Satoshi Kura

Title: A Category-Theoretic Framework for Dependent Effect Systems

Abstract: Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning about effectful computations. However, existing categorical frameworks for graded monads do not support effects that may depend on program values, which we call dependent effects, thereby limiting their expressiveness. We address this limitation by introducing indexed graded monads, a categorical generalization of graded monads inspired by the fibrational ``indexed'' view and by classical categorical semantics of dependent type theories. We show how indexed graded monads provide semantics for a refinement type system with dependent effects. We also show how this type system can be instantiated with specific choices of parameters to obtain several formal systems for reasoning about specific program properties. These instances include, in particular, cost analysis, probability-bound reasoning, expectation-bound reasoning, and temporal safety verification.

• 12:00-12:30: Takumu Nakamura

Title: Modular Construction and Analysis of a Compositional Gradient-Based Learning Method

Abstract: Two prior works apply category theory to the construction of gradient-based learning algorithms, both using parametrized lenses to model learning.

The construction of Fong et al. provides functoriality, whereas that of Cruttwell et al. offers modularity and greater generality.

In this paper, we modularize and generalize the functorial construction of Fong et al. by adopting the modular and generic principles underlying the approach by Cruttwell et al.

This generalization allows us to accommodate optimizers and loss functions used by Cruttwell et al., which were not supported in the original functorial setting.

We also give a modular proof method of a consistency property of our learning algorithms, namely the GetPut law as lenses, serving also as an application of our modularization.

Moreover, the modular design enables us to easily adapt our framework to handle a loss function for classification tasks, namely softmax cross-entropy.

• 12:30-14:00: Lunch Break 

• 14:00-14:30: Masahiro Hamano

Title: De Finetti’s Exchangeablity in Exponentiality of a Stochastic Category

Abstract: A famous De Finetti ’s Theorem (30s) establishes a unique correspondence between infinite exchangeable random variables and a probability distribution over probability measures, which governs their joint distributions for any finite processes. This talk presents a category- theoretic account of De Finetti ’s exchangeability, using the notion of a stochastic exponential comonad recently studied by Hamano (’23). We show that the exponential measurable space, constructed as the limit of tensor folding equalisers, provides a categorical framework to es- tablish the theorem in terms of Giry monad composition inherent in our stochastic kernels. Our construction employs the free exponential construction of Mellies-Tabareau-Tasson, but is not free as projections between equalisers represent specific “ pick-and-discard ” sampling operations. The limit measurable space is given by certain cylinder sets approximated by the exponential limit of the sigma field over finite multisets. Although it may not cover all the class of the exchangeable r.v’s, our framework is shown to subsume De Finetti ’s original theorem for binary r.v’s in terms of Bernoulli distribution, since the resulting exponential measurable space is dense in the interval [0,1] picking a distribution parameter.

• 14:30-15:00: Arthur Gall 

Title: A Categorical Leibniz Rule for Transition Systems and Its Application to Probabilistic Programs

Abstract: Inspired by derivations on semirings and algebras, we define a notion of derivation in any category C with finite biproducts, satisfying a Leibniz rule for composition. We show that the category TS(C) of transition systems over C inherits both biproducts and derivations. Our motivating application is differentiating parametrized Markov chains: taking C to be a category of parametrized signed measures, the derived transition system provides a pathwise algorithm for Monte Carlo gradient estimation, which might avoid costly symbolic computation of output distributions. We are also interested in understanding whether our derivation can be generalized to a differential operator, connecting to the broader theory of differential categories, and look forward to discussing this with the workshop participants.

• 15:00-15:30: Afternoon Break 

• 15:30-16:00: Jad Koleilat

Title: A Fibrational Perspective on Differential Linear Logic

Abstract: Differential Linear Logic (DiLL) is a sequent calculus expressing differentiation through symmetries between linear and non-linear formulas. In this talk, we express categorical models of DiLL as a pair of Grothendieck fibrations equipped with a tangent functor. To do so, we adapt methods from categorical semantics of type theory to linear-non-linear adjunctions. In the future, we hope this approach will enable the construction of models of what could be called dependent differential linear logic.

• 16:00-16:30: Isaiah B. Hilsenrath

Title: Monoidal Differential Turing Categories

Abstract: Just as simply typed lambda-calculus is sound and complete with respect to Cartesian closed categories by the Curry-Howard-Lambek correspondence, simply typed differential lambda-calculus is sound and complete with respect to Cartesian (closed) differential categories. In a 2019 paper, Cockett and Gallagher refined these ideas to provide a categorical semantics of the untyped differential lambda-calculus, introducing the Cartesian differential Turing category with differential canonical codes. This coherently combined a Cartesian differential category with a type of category that provides a sound and complete semantics for the ordinary untyped lambda-calculus: a (total) Turing category with canonical codes. Now, an important source of examples of Cartesian differential categories comes from the categorical semantics of differential linear logic: monoidal differential categories. The coKleisli category of a monoidal differential category is a Cartesian differential category. It is then natural to ask what is the analogue of a monoidal differential category whose coKleisli is a Cartesian differential Turing category. In this talk, I will introduce monoidal differential Turing categories and their analogous notion of differential canonical codes, investigate their properties, show examples of such categories, and ultimately, show that the coKleisli category of a monoidal differential Turing category (with differential canonical codes) is indeed a Cartesian differential Turing category (with differential canonical codes).

• 19:00: Conference Dinner

• 9:00-10:00: Robin Cockett

Title: Curve objects in tangent restriction categories

Abstract: The last section of Geoff Cruttwell and my 2013 paper on Tangent Categories is dedicated entirely to axiomatizing restriction tangent categories (that is partiality in tangent categories).  Disappointingly, however, this aspect of tangent categories has not received as much attention as we expected.   This is a little surprising as all the traditional areas such as differential geometry, algebraic geometry, analysis, and computability have foundational aspects of partiality.  

The purpose of this talk is to recall the definition of tangent restriction categories and, furthermore, to take a look at curve objects in tangent join restriction categories.  This will cause us to dig quite deeply into the frame theoretic aspects of the setting.

• 10:00-11:00: Morning Break 

• 11:00-11:30: Geoff Vooys

Title: A Tangent Categorical Perspective on Immersions and Unramified Morphisms

Abstract: Two of the most important concepts in differential and algebraic geometry are those of immersions (maps which are injective at the level of tangent spaces) and unramified morphisms (maps which do not have tangent vectors ramify over any point). In this talk, based on joint work with JS Lemay, I will define unramified morphisms and three different strengths of immersions at the tangent-categorical level and present examples of how these morphisms behave and incarnate in many tangent categories of interest to mathematicians and computer scientists. We will conclude the talk by showing that in complete generality for tangent categories, the classes of immersions and unramified maps need not coincide.

•  11:30-12:00: Florian Schwarz

Title: Dimensions and the universality of the vertical lift

Abstract: The universality of the vertical lift is a key, but somehow unintuitive, part of the axioms defining a tangent category. In this talk I will introduce a generalized notion of dimension that will give intuition on the meaning of the universality of the vertical lift. A short calculation will show that for this generalized notion of dimension, the equation $\dim(T^2(X)) + 2 \cdot \dim (X) = 3 \cdot \dim(T(X))$ needs to hold in any tangent category. I will show examples of this notion of dimension that go beyond the classical dimension of manifolds and vector spaces. In particular I will use dimension to prove that the only Cartesian tangent structures on Set$^\mathrm{op}$ is the trivial one.

• 12:00-12:30: Marcello Lanfranchi

Title: The formal theory of tangentads

Abstract: Tangent categories offer a categorical context for differential geometry, by categorifying geometric notions like the tangent bundle functor, vector fields, Euclidean spaces, vector bundles, connections, etc. In the last decade, the theory has been extended in new directions, providing concepts such as tangent monads, tangent fibrations, tangent restriction categories, reverse tangent categories and many more.

It is natural to wonder how these new flavours interact with the geometric constructions offered by the theory. How does a tangent monad or a tangent fibration lift to the tangent category of vector fields of a tangent category? What is the correct notion of vector bundles for a tangent restriction category? We answer these questions by adopting the formal approach of tangentads, which provides a unifying context for tangent category theory.

After introducing the notion of tangentads, we show how to construct formal notions of vector fields, differential bundles, and connections for tangentads and extend some classic results to the formal setting. We show that vector fields form a Lie algebra and that differential bundles over the terminal objects are equivalent to differential objects. Finally, we construct vector fields and connections using PIE limits and compute these constructions for some examples.

This project is covered in:

Tangentads: a formal approach to tangent categories

https://arxiv.org/abs/2503.18354

The formal theory of tangentads PART I

https://arxiv.org/abs/2509.15524

The formal theory of tangentads PART II

https://arxiv.org/abs/2601.15534

• 12:30-14:00: Lunch Break 

• 14:00-14:30: Ken Sakayori

Title: Wiring the Pi-calculus to Denotational Semantics

Abstract: It is well known that pi-calculi are closely connected to relational models, the simplest models of DiLL, as well as to linear logic proofs and game semantics. However, these connections are typically established through substantial modifications of the pi-calculus, since processes do not naturally form a category under the standard operational theory. In this talk, I will present AWpi, a dialect of the asynchronous pi-calculus with a simple type discipline: each input name may be owned by at most one process. AWpi yields a category whose objects are types, morphisms are AWpi processes (modulo barbed congruence), and identities are special processes called wires. Furthermore, from the category of processes, we can carve out a relative Seely category by drawing on insights from game semantics. At the same time, AWpi follows the tradition of ordinary pi-calculi in that expressiveness is preserved and the operational theory is developed in a similar manner. If time allows, I will informally discuss whether we can extend this picture to encompass differential nets/categories while remaining faithful to the operational tradition of the pi-calculi. (This talk is based on a joint work with Davide Sangiorgi, Simon Castellan and Pierre Clairambault)

• 14:30-15:00: Richard Blute

Title: Quantum Finiteness Spaces

Abstract: A result of Coecke, Pavlovic and Vicary states that a finite-dimensional Hilbert space can be equivalently characterised as a commutative dagger-Frobenius monoid in the category of finite-dimensional Hilbert spaces. This can be extended to an equivalence between such Frobenius algebras and the category of finite sets.

We describe an ongoing project to attempt to extend this result beyond finite sets. This requires on the one hand replacing the category of sets with the category of Ehrhard’s finiteness spaces, one of the motivating examples for the theory of differential linear logic. On the other hand, Frobenius algebras must be replaced by linear monoids in the sense of Priyaa Srivinvasan. 

Joint work with Durgesh Kumar & J.S. Lemay

• Tomoaki Abuku, Gifu University

• Kazuyuki Asada, Tohoku University

• Richard Blute, University of Ottawa

• Robin Cockett, University of Calgary

• Soichiro Fujii, National Institute of Informatics

• Zeinab Galal, RIMS, Kyoto University

• Arthur Gall, National Institute of Informatics

• Andrea Giusto, University of Genoa

• Masahiro Hamano, National Cheng Kung University 

• Masahito Hasegawa, RIMS, Kyoto University

• Ichiro Hasuo, National Institute of Informatics & Imiron Co., Ltd.

• Isaiah B. Hilsenrath, University of Pennsylvania

• Ryuya Hora, TBD

• Keisuke Hoshino, Kyoto University 

• Yuki Imamura, Osaka Metropolitan University

• Shin-ya Katsumata, Kyoto Sangyo University

• Yuto Kawase, RIMS, Kyoto University

• Marie Kerjean, LIPN

• Sangwoo Kim, University of Tokyo

• Jad Koleilat, Université Sorbonne Paris Nord

• Mayuko Kori, RIMS, Kyoto University

• Rose Kudzman-Blais, RIMS, Kyoto University

• Satoshi Kura, Waseda University

• Marcello Lanfranchi, Macquarie University

• Jean-Simon Pacaud Lemay, Macquarie University

• Yuki Maehara, Tokyo Metropolitan University

• Takumu Nakamura, Tohoku University

• Ken Sakayori, The University of Tokyo

• Takahiro Sanada, Fukui Prefectural University

• Florian Schwarz, University of Calgary

• Thomas Seiller, CNRS

• Takeshi Tsukada, Chiba University

• Holger Thies, Kyoto University

• Jean-Baptiste Vienney, University of Ottawa

• Geoff Vooys, TBD

• Aymeric Walch, ISAE-Supaero