Seminars

I will give an introduction to alifib, an experimental programming language founded on higher-dimensional rewriting, and demonstrate a web-based proof assistant built around it.

alifib implements a minimal type theory in which the only types that exist are directed higher inductive types. Terms are assembled as pasting diagrams of generators. Semantically, the types are finite directed complexes, which have a dual nature of "combinatorial cell complexes" and "higher-dimensional rewrite systems". These are extremely versatile structures, allowing for disparate uses of the language ranging from "proof-relevant equational reasoning in categorical structures", to "specification of abstract machines with witnesses for their computational traces" through "computation of the homology of finite cell complexes". Time permitting, I will demonstrate examples of each of these uses.

The proof assistant gives access to analysis of types, diagrams, and maps, as well as string-diagram-driven interactive rewrite sessions. Thanks to the “computation-as-higher-diagram” paradigm, all proofs constructed interactively can be committed to code as alifib terms, providing a uniform, semantics-driven text format for diagrammatic proof witnesses.

The alifib web interface (still under heavy development) is served at https://ahadziha.github.io/alifib/ . This is an ARIA-funded project with contributions from Alex Kavvos, Diana Kessler, and Wessel de Weijer.

This work uses LLMs as a natural language interface to a musically rigorous generative system rooted in Xenakis' theory of Markovian Stochastic Music, a framework in which compositional structure emerges from stochastic processes governed by probability transition matrices. Rather than allowing an LLM to generate arbitrary musical output, the system constrains generation through a domain-specific language (DSL) built on top of Tidal Cycles, a live coding environment embedded in Haskell. The functional programming substrate provides a natural setting for expressing compositional rules as composable, typed abstractions, while the Xenakis framework supplies the musical semantics. The central hypothesis is that this combination of disciplined abstraction — functional structure below, stochastic music theory above — enables LLMs to produce coherent musical output, avoiding pitfalls such as low-level syntactic errors, hallucinated sample banks, and other inconsistent behaviour typical of unconstrained generation.

Normalization, D(X + 1) → D(X) + 1, is almost a distributive law; but because one of the distributive law axioms only holds up-to-idempotent, it only yields a non-associative composition of normalized kernels. This talk has two goals. The first is to develop the formal category theory abstracting normalization: how a failing distributive law still induces a monoidal magmoid, and how monoidality and commutativity differ in this setting. The second is to explore probability theory internal to this magmoid of normalized kernels: how the lack of associativity leads to two distinct modes of inference. This is joint work with Elena Di Lavore and Márk Széles (https://arxiv.org/pdf/2510.01131).

A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates---used to establish semantic termination arguments---to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

Over the past few years a view of categorical systems theory based on double categories has emerged. We show how to incorporate labelled models of concurrency as an instance of this systems theory. Winskel and Nielsen have argued that the functor that maps each concurrent system to its underlying set of labels is an ambifibration, i.e. both a partial fibration and a partial opfibration. We show that an ambifibration which is a split opfibration over its base category corresponds precisely to a double functor from a double category of spans whose left legs have cartesian lifts. As an intermediate step we establish the universal property of the double category of spans over an adequate triple. Our construction enables turning such an ambifibration into a loose right module over a category of spans, which amounts to an instance of Libkind and Myers’ Double Operadic Theory of Systems (DOTS). As an example we explore the structure of this instance for Labelled Transition Systems (LTSs).

Past and future light cones arise as an important side-effect of the theory of relativity. One can abstract this aspect — the theory of light cones -- into what Chris Heunen and Nesta Van Der Schaaf called "ordered locales". The talk will introduce this theory describing, in particular, the "causal order" induced by these cones. The talk will then focus on the theory of trajectories — and their homotopy — arising from ordered locales.

Absolutely no knowledge of physics or relativity is required!

The no cloning theorem in quantum mechanics states that an arbitrary quantum cannot be cloned. In the categorical formulation of finite dimensional quantum mechanics, this means that there is no family of natural diagonal morphisms in a dagger compact closed category. However, if we drop naturality, we can always clone a given orthonormal basis, which defines a dagger Frobenius algebra structure on the underlying Hilbert Space. The comultiplication map of this algebra encodes the basis as the copyable elements. Moreover, every dagger Frobenius algebra on a finite dimensional Hilbert space is of this kind.

It was conjectured by Prof Richard Blute (U of Ottawa) that a similar correspondence would hold in a model of mixed unitary categories- given by (reflexive) Lefschetz spaces. In this talk, we will give a functorial construction of a finiteness space starting with a reflexive Lefschetz space with a basis by studying the support of convergent nets of finite sums over the basis vectors. We will prove that, on objects, this construction is inverse to Ehrhard's construction of a Lefschetz space from a finiteness space. We will use the support construction and Ehrhard's construction to establish an adjunction between the category of finiteness spaces (with functions) and the category of dagger linear semigroups in reflexive Lefschetz spaces (with cosemigroup morphisms).

Finally, we give a class of examples of cosemigroup structures whose copyables don't span the space, thus contrary to the conjecture, this coreflection fails to be an equivalence.

Categorical Message Passing Language (CaMPL) is a functional concurrent programming language whose semantics is in category theory.

In Part 1, we discussed the core programming features of CaMPL: the concurrent part (channels and processes), sequential part (messages and functions that compute messages), and message passing (communication between processes along channels). In this talk, we will discuss more programming features: non-deterministic processes which are implemented using races,higher-order processes which pass other processes as messages, andsession types which are implemented as custom channel datatypes called protocols and coprotocols.

In the last talk, we concluded with a demonstration of a program in which 2 clients send messages to a server in a pre-determined order. We observed that this system was not truly concurrent as the server was deterministic, i.e., it waited for client 1 to send a message before it could receive a message from client 2. In this talk, we will solve this problem using the “race” command. This feature allows CaMPL to program booking systems.

CaMPL also supports higher-order message passing. This means that a process can be encoded as sequential data and sent as a message to another process which then can execute the encoded process. This feature allows CaMPL to program app stores which distribute code to other processes.

As a demonstration of protocols and coprotocols, we will showcase a program in which two processes are connected by a channel that can be split/forked arbitrarily many times. This feature allows CaMPL to program server processes that continue running indefinitely and accepting new connections with client processes.

We will briefly explore the categorical semantics of these programming features. However, the focus of this presentation will be on the code demonstrations. The categorical semantics of “race” (non-determinism) is obtained by enriching the core semantics in sup-lattices to replace the process hom-sets with hom- power-sets.The higher-order categorical semantics is obtained by enriching the core semantics in the category of messages, so the processes also exist as messages that can be sent.The categorical semantics of (co)protocols are given by inductive and coinductive datatypes.We will briefly introduce the concepts of enrichment and inductive and coinductive datatypes.

The starting point of algebraic language theory is that regular languages of finite words are exactly those recognized by finite monoids. This finiteness condition gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. In this work, we move from words and monoids to trees and clones, the algebraic structures underlying deterministic bottom-up tree automata. Using the categorical notion of codensity monad, we introduce a profinite completion for clones. We prove that this construction simultaneously generalizes the ultrafilter monad on sets and the profinite completion of monoids. When applied to free clones on a ranked alphabet, the profinite completion of clones yields a notion of profinite tree, providing a topological approach to regular languages of finite trees. We prove that these profinite trees coincide with a well-identified fragment of the profinite lambda-calculus, and we characterize this fragment via a parametricity theorem.

Categorical Message Passing Language (CaMPL) is a functional concurrent programming language, and the semantics of its programming features are defined in category theory.

In this talk, we explore the categorical semantics of the core programming features in CaMPL, and we will demonstrate example programs to showcase these features. This will include the concurrent part (channels and processes), sequential part (messages and functions), and message passing (communication between processes along channels).

The categorical semantics of message passing is given by a linear actegory in which the sequential part acts on the concurrent part in two directions. This allows messages to travel along channels in two directions. We will introduce the concepts of linearly distributive categories and linear actegories in a beginner-friendly way.

The tacit (point-free) way of programming is to write functions without naming variables and intermediary values. We have two styles for that: Applicative and Compositive. In this talk, I will introduce both styles, as well as models for them (Combinatory Logic and Concatenative Calculus) and show that these styles are relatable (pun).

The codensity monad of the functor including the category of finite sets into that of all sets is the ultrafilter monad, whose category of algebras is the category of compact Hausdorff spaces. This is surprising: by applying a general category-theoretic construction, it is possible to get from the world of finite sets to the world of spaces. An overview of these facts is in [Leinster, 2013]. A separate fact, proved in [Garner, 2020], is that the Vietoris monad, a powerset-like monad on compact Hausdorff spaces, can be constructed by a weak distributive law of the ultrafilter monad over the powerset monad. The following suspicion arises: is it possible to construct this weak distributive law from the world of finite sets in parallel with the codensity construction of the ultrafilter monad? We will give an introduction to the main suspects and describe the clues that lead us to this suspicion.

The aim of this talk is to express the fully algebraic theory of monoidal bicategories as developed in the 1990's by Kapranov-Voevodsky, Baez-Neuchl, Day-Street and many others in the essentially homotopical language of higher algebra as developed in the 2010's by Lurie. We show that the theory of E_n-operads, which originates from May's geometric classification of $n$-fold loop spaces, provides a convenient way to handle concepts in both areas.

Indeed, we prove that braided, sylleptic and symmetric monoidal bicategories, in the sense of Day and Street, are exactly the E_n-algebras, for $n = 2, 3, 4$, respectively, in the sense of Lurie.

The proof of this result involves a study of the infinity-category of bicategories and subsequent subtle considerations on partial homotopy-coherent associative structures known as A_n-algebras. As an application, we give a conceptual proof of the bicategorical version of the fact that monoids in a (symmetric) braided monoidal category form a (braided, and in fact symmetric) monoidal category.

In this talk, I will introduce the theory of scroll nets, which is a novel diagrammatic formalism for representing proofs and programs. As the name indicates, it is based on the « scroll », a notation for logical implication invented by Charles S. Peirce at the end of the 19th century for his system of existential graphs, to which it adds a graphical syntax inspired by proof nets to represent inference rules. I will first motivate the notation from a philosophical standpoint, arguing that it captures the smallest motions of deductive reasoning in the most natural way. I will then show how it captures minimal implicative logic by simulating the rules of natural deduction. Through the Curry-Howard correspondence, this will lead us to identify a notion of detour/redex that generalizes that of simply-typed λ-calculus, making scroll nets into an expressive computational framework. If time remains, I will illustrate how to capture classical logic, as well as intuitionistic disjunction and co-implication by considering horizontal and vertical generalizations of the scroll.

We investigate the connection between automata theory and λ-calculus in terms of syntax, semantics and logic. A starting point for this investigation is Salvati’s notion of language of λ-terms recognized by a cartesian closed category, which generalizes to the higher-order setting the usual regular languages of finite words and trees.

First, we extend Salvati’s work by showing that all well-pointed, locally finite non-posetal cartesian closed categories recognize the same languages of λ-terms as the category of finite sets, which we call higher-order regular languages. In turn, we extend the syntactic approach of Hillebrand and Kanellakis to the higher-order setting, and show that the obtained languages coincide with higher-order regular languages, hence connecting our work to the implicit automata research program of Nguyễn and Pradic. This demonstrates the robustness of the notion of higher-order regular language.

Second, we take inspiration from ideas coming from Stone duality and introduce profinite λ-terms, a higher-order generalization of the notion of profinite word. The space of profinite λ-terms can be equivalently described in three ways: as a metric completion, as the Stone dual of the Boolean algebra of higher-order regular languages, and through parametricity à la Reynolds. Profinite λ-terms assemble into a cartesian closed category that verifies a universal property with respect to certain Stone-enriched categories; this amounts to a semantic interpretation of the profinite λ-calculus.

Recent developments in higher category theory suggest a directed form of algebraic topology or homotopy theory. In this framework, one studies (pointed) (∞,∞)-categories in place of (pointed) spaces, directed analogues of the loop–suspension adjunction, categorical spectra equipped with the Gray smash product, stable Gray categories,... (see e.g. [https://nmasuda2.github.io/notes/thesis_stable.pdf], [arXiv:2505.22640], [arXiv:2508.16787]).

A key ingredient in the theory of “directed spaces” (=(infty,infty)-categories) is the notion of fibrations (in the sense of a Grothendieck construction). For (∞,1)-categories, (co)cartesian fibrations admit a clean internal formulation via relative adjunctions. For (∞,n)-categories (including n = ∞), a definition of fibrations also exists (e.g. arXiv:2108.11431, arXiv:2307.11931) but one lacks a definition that can be given internally. We conjecture that just as adjunctions govern fibrations in the (∞,1) world, lax n-adjunctions may be used to give an internal definition of fibrations in the (∞,n) world. This would yield a notion of higher fibrations internal to any (∞,n+1)-category (with the right limits), and potentially enable the definition of higher Grothendieck topoi via fibrational descent (cf. [arXiv:2410.02014] for the (∞,2)-case).

In this talk, we will review the basics of (∞,∞)-categories, sketch a definition of lax n-adjunctions and the walking lax ∞-adjunction, and indicate how these structures relate to fibrations. Time permitting, we will also discuss analogues of this in a Gray setting (aka (∞,∞,1)-categories).

This is based on work in progress with Marcus Nicolas.

There is a huge variety of objects which deserve the name "dynamical system". Most important types fit into the framework called "double categorical systems theory", developed by Myers. In this framework, the trajectories of a dynamical systems are defined to be the homomorphisms of systems out of specified "clock systems" - for example, a trajectory of a discrete dynamical system is a homomorphism out of the dynamical system (N,+1). Describing clock systems for notions deterministic dynamical system is relatively straightforward, but their description for stochastic systems is more complicated. For discrete-time stochastic dynamical systems - that is, Markov chains - this was recently resolved, but the solution does not apply to continuous-time stochastic processes, such as SDEs (stochastic differential equations). In addition to giving an introduction to all of the preceding, I'll present some work in progress on defining clock systems for SDEs.

Whenever an algebraic structure is defined via a presentation A = < X | R>, a fundamental question arises: how can we tell if two elements generated from X are equal as elements in A? For commutative algebras, this was answered by Buchberger more than fifty years ago, using Gröbner bases. His seminal work has since been applied to many “classical” linear algebraic structures, including associative algebras.

In this talk, we explain how to extend Gröbner bases to linear 2-categories, taking insights from higher rewriting theory. Our approach is rooted in practical problems coming from representation theory and low-dimensional topology. We will emphasize differences with the classical setting as well as open directions of research.

In this talk, I will present my MSc Thesis work on the homotopy theory of equilogical spaces, motivated by the search for models of impredicative univalent type theory. The category of equilogical spaces is equivalent to the subcategory of modest sets in a realizability topos, which in particular makes it a model of impredicative type theory. But equilogical spaces furthermore admit a simple definition as (T0, countably-based) topological spaces equipped with equivalence relations, so in particular also carries homotopical content via the topology, i.e. where the notion of homotopy is induced by the real unit interval [0, 1] in the usual way. Therefore, (one wishes that) a homotopy theory of equilogical spaces should yield a model of impredicative univalent types.

It turns out that the category of equilogical spaces (and also its enveloping realizability topos) is already a homotopy category where the equivalence relation gives the notion of path. So a proper treatment of the homotopy theory of equilogical spaces requires us to “fuse” two notions of path: one given by the equivalence relation, and the other one given by the topology. I will present my attempts at constructing a homotopy theory fusing these two. Along the way, I also explore the homotopy theory of QCB (Quotient of Countably-Based) spaces, which are exactly the topological spaces obtaining by sending an equilogical space (X, ~) to its resulting quotient X/~. Here, I obtain a Quillen model structure on QCB spaces in which the weak equivalences are homotopy equivalences. This model structure looks exactly like the Strøm model structure on the category of topological spaces.