A weekly, informal seminar on topics relevant to the Topos Institute Community, held in-person at our Oxford Campus.
You can find links to the recordings of the talks and accompanying slides (when available) below. You can also view a YouTube playlist of all recordings.
If you would like to subscribe to the mailing list for this seminar to receive updates about upcoming talks you can do so by sending a blank email to oxford-seminar+subscribe@topos.institute.
A complex system may be designed modularly by putting together interacting component subsystems. Since analyses of complex systems can often scale very poorly with their size, it pays to use the modular structure of such systems to divide the task of analysis across the component subsystems.
Many analyses of systems may be encoded as homomorphism search problems between systems of the same sort. This suggests attending to categories of systems and their homomorphisms. In this talk, we’ll consider the modular structure of a class of systems as a 2-algebra — an algebraic structure on categories of systems (and their interfaces and interaction patterns). We’ll see compositionality theorems as (lax) homomorphisms of these 2-algebraic structures, and survey a number of techniques for proving them using 2-categorical algebra.
Which results on gender and science every mathematician should know
Olga Paris-Romanskevich 30th of April, 2026
Based on a selection of works in social psychology, sociology and cultural studies, I will discuss several epistemological approaches of how one can think the exclusion of women and gender minorities from sciences and mathematics in particular. In the discussion following the talk, we will collectively approach what can be done, at the individual and collective level, in order to prevent violence and exclusion from happening.
An introduction to the geolog project
Owen Lynch
(Topos)
2nd of April, 2026
Within the ARIA program, a number of researchers are working on a project called “geolog.” Geolog has some ambitious goals and some controversial theses; in this talk we will give an overview of these goals and theses alongside an intro to some of the math and computer science that we are using to attempt to achieve the goals and confirm the theses.
Particle Filters and Factor Graphs for Narrative Space: A Compositional Framework for Scenario Analysis
Wesley Phoa 19th of March, 2026
We develop a formal framework for scenario-based analysis in which narratives—structured accounts of how a situation might evolve—are treated as hidden Markov models whose latent states are explored via particle filters. The framework, introduced in an earlier paper for television series architecture, extends naturally to real-world scenario analysis: geopolitical, technological, and financial narratives whose state spaces interact. When multiple narratives are analyzed independently, their interdependencies remain implicit. We show that these dependencies can be made explicit using factor graphs, and that the resulting compositional structure has a natural interpretation in the language of decorated cospans and operads. The category- theoretic formalization is not ornamental: it provides the algebra for composing open narrative systems along shared interfaces, and it scales to the many-narrative setting that real-world scenario analysis requires. We illustrate with the push to democratise private markets—four interacting narratives whose factor graph reveals a self-reinforcing loop that is also, traced in the other direction, a self-destructing one—and interpret their factor graph as a colimit in a category of open systems.
Why might I want to build a formal model for a respiratory virus?
Tim Hosgood
(Topos)
12th of March, 2026
At the risk of giving a talk completely lacking structure, I’d like to jump around a bit and try to answer a few different questions:
How can formal modelling software, like CatColab, help people to better understand scientific models outside their expertise?
What do we mean when we say things like “categorical modelling can help make assumptions explicit”?
How can we allow for somewhat informal-looking diagrams to convey precise quantitative information?
What does it look like, in practice, to add new functionality to CatColab?
In reality, of course, I spent weeks before I realised that these were actually the questions that I was interested in, let alone before I was able to come up with some answers. Here, I’ll try to disentangle things a bit and present a cleaner story.
This talk will be split into two parts: the first 45 minutes will be for a general audience, followed by a 20 minute technical discussion with a brief coffee break in between.
Categorical systems theory: control and emergence
David Corfield 5th of March, 2026
This will be an informal session with plenty of discussion time, investigating a couple of concepts that arise from the category-theoretic treatment of systems.
(1) Control
How inputs to a system regulate its behaviour. Starting points: (a) In response to the ‘active inference’ program, some recent articles (e.g., https://arxiv.org/abs/2406.07577 and https://arxiv.org/abs/2508.06326) have looked to understand autonomous systems as composed of agent and controller subsystems, equipped with dual interfaces; (b) Ordinary Lyapunov functions have been treated category-theoretically (https://arxiv.org/abs/2502.15276), work that should be extendable to variants. Where ISS (input-to-state stability) Lyapunov functions concern stability under any external perturbation, control Lyapunov functions concern stability under a chosen input.
(2) Emergence
Phenomena where the composite behaviour of the parts does not equate to the behaviour of the composite. Starting points: (a) Elie Adam’s thesis, ‘Systems, Generativity and Interactional Effects’ (https://elieadam.com/eadam_PhDThesis.pdf); (b) Puca et al. on ‘Failures of compositionality’ (https://arxiv.org/abs/2307.14461) (c) Erik Hoel on causal emergence (e.g., https://arxiv.org/abs/2202.01854). Two relevant CT constructions appear to be laxness of functors and coarse-graining as epimorphisms, potentially fitting well with a double category-theoretic outlook.
A glance at Petri net theory
Adrián Puerto Aubel
(University of Oxford)
19th of February, 2026
Petri nets are formal models of computing well-known for depicting true concurrency. Unlike automata, they overcome the state-space explosion problem by avoiding interleaving semantics. In this talk I will give an overview of the most prominent theoretical developments of more than 50 years of Petri net theory. This will range from the different expressions of formal semantics of these models as marking graphs, unfoldings, or event structures, to an overview of relevant problems defined on them and their complexities, with a particular focus on structural analysis techniques.
No matching items
A Second Taste of Quantitative Logic
Matteo Capucci 4th of December, 2025
In this second talk I will introduce p-means and argue they form a good quantitative analogue of first-order quantifiers. I will then sketch the construction of a hyperdoctrine valued in enriched graded preorders which forms the intended semantics of a first-order quantitative linear logic.
A Taste of Quantitative Logic
Matteo Capucci 26th of November, 2025
Quantitative logic, after Lawvere, is one whose judgments are valued in real numbers, rather than merely being a logic about real numbers. By doing this we can guarantee good structural properties of the logic, such as being able to treat addition as an additive connective in the sense of Girard. Moreover, by employing the full spectrum of sums multiplication distributes over, we are able to approximate ‘hard’ connectives with ‘soft’ ones, with application in machine learning. In the talk I will showcase these features by describing a sequent calculus for a quantitative version of linear logic. This is work in progress with Atkey, Grellois, and Komendantskaya.
Program logics via distributive monoidal categories
Elena Di Lavore
(University of Oxford)
6th of November, 2025
We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. Rules of program logics are derived from this categorical structure.
Accepting Normalization in Markov Categories
Mario Román
(University of Oxford)
30th of October, 2025
Normalization of probability distributions is not a distributive law, and normalized kernel composition does not define a category. This talk aims to highlight these limitations and take an alternative route: we will introduce distributive sesquilaws and, from their axioms, derive some of the properties of normalization. In particular, we will see how normalized kernels form a unital magmoid with an action of the category of subdistributions, and we will recap its possibilistic analogue: the action from may-must relations into the category of relations. In this sense, the magmoid of normalized kernels is the stochastic analog of the category of relations. The talk is based on joint work with Elena Di Lavore, Paweł Sobociński, and Márk Széles (arxiv.org/pdf/2502.03477, arxiv.org/pdf/2510.01131).
Descent in Probability Theory: the first steps downward
Paolo Perrone
(University of Oxford)
16th of October, 2025
Coarse-graining, forming quotients by dropping distinctions, is a unifying idea across mathematics: identifying the endpoints of an interval yields a circle; groups are conveniently presented as quotients of free ones; sheaves and stacks emerge from gluing local data. This idea is also central to probability, where “observing” a random variable similarly quotients a sample space via the sigma-algebra it generates (and is crucial for modeling randomness as “ignorance”). Yet this quotienting procedure, in probability, has so far lacked a systematic categorical treatment.
We develop a descent theory for probability that makes this intuition precise, while respecting probabilistic practice as much as possible. On the category theory side, the theory parallels classical descent, but diverges in a few ways due to the presence of stochastic dependence (correlations). On the probability side, it unifies the three core concepts of measurability, disintegration and stochastic dominance, within a single framework, providing conceptual understanding of the relationships between random variables, statistical experiments, and inference procedures.
Wreaths in Span(Set)
Jason Brown
(Topos)
2nd of October, 2025
Steve Lack and Ross Street introduced wreaths as a generalisation of distributive laws between monads in their paper The formal theory of Monads II. This paper presents a nice story about how wreaths arise from considering the free completion of a 2-category under Kleisli objects and provides some interesting examples of wreaths. In particular, it is shown that orthogonal factorisation systems on a category can be expressed as wreaths in \mathsf{Span}(\mathsf{Set}).
In this talk we’ll try to understand general wreaths in \mathsf{Span}(\mathsf{Set}) as expressing a weaker notion of factorisation system on a category. We’ll relate these factorisation structures to both familial functors and crossed double categories, and also present examples of where they naturally occur.
Khyathi Komalan
(California Institute of Technology)
25th of September, 2025
The internet is a strange place — one moment you’re convinced the Starbucks logo never had a star on top, the next you’re knee-deep in a rumor that spreads everywhere at once, and before long you’re staring at a series of pictures that “prove” the moon landing was fake. These phenomena may look like pure nonsense, but they also show how perception, memory, and belief are shaped by our experiences, the hidden biases behind what we perceive, and the difficulty of stitching multiple pieces of information, sometimes conflicting, into a coherent story that fits the most into one’s worldview.
In this talk I introduce “adult brainrot” as a categorical framework for these inconsistencies. I will show how categorical models of quantum processes can capture order-sensitive memory and indistinguishable sources of misinformation, and how categorical notions of centers help explain why people’s theories sometimes fail to form a consistent picture of reality. The aim is to argue that quantum categorical structures offer a natural mathematical framework for modeling the inconsistencies and oddities of human perception and belief.
Free PLTL Algebras and A Coalgebraic LTL Extension of Hyperdoctrines
Q Le
(University of Oxford)
18th of September, 2025
In this seminar, I describe the work I had done over the summer of 2025 at the Topos Institute with José Vitor Paiva Miranda de Siqueira. Inspired by the free Boolean/Heyting algebra of a given set, we develop a free-forgetful adjunction between posets and PLTL temporal algebras, where PLTL denotes propositional linear temporal logic. We provide a description of their induced Eilenberg-Moore categories. We describe how this could be used to temporalise systems and logics through hyperdoctrines and connect this to the stream comonad. We end with future research directions, connecting this topic with the cofree comonad of polynomial functors and temporalising doxastic logic.
Compositionality of Flavoured Petri Nets
David Jaz Myers
(Topos)
11th of September, 2025
In this talk, we will see a natural notion of nesting composition for “flavoured” Petri nets: Petri nets whose places and transitions come with extra data determined by a symmetric monoidal double category and which determine the intended semantics of the Petri net.
Oxford Office short talks
José Siqueira, Q Le, Khyathi Komalan 4th of September, 2025
José: Given a base logic with predicates on states, there are two tasks one might want to accomplish simultaneously: add in a notion of dynamics to the states (which is done comonadically), and enhance the logic used (which is achieved by a determining a monad on posets). I’ll sketch how specifying a lax morphism of monads with a hyperdoctrine as its underlying functor provides a base semantics for enhanced (e.g., temporal) formulae on behaviours of systems, which then induce a new hyperdoctrine whose contexts are the systems themselves.
Q: Linear error-correcting codes form the mathematical backbone of modern digital communication and storage systems, but identifying champion linear codes (linear codes achieving or exceeding the best known minimum Hamming distance) remains challenging. By training a transformer to predict the minimum Hamming distance of a class of linear codes and pairing it with a genetic algorithm over the search space, we develop a novel method for discovering champion codes. This model effectively reduces the search space of linear codes needed to achieve a best minimum Hamming distance. Our results present the use of this method in the study and construction of error-correcting codes, applicable to codes such as generalised toric, Reed–Muller, Bose–Chaudhuri–Hocquenghem, Algebraic–Geometry, and potentially quantum codes.
Khyathi: Fusion categories capture finite particle-like excitations and their fusion rules. I will briefly recall their motivation and then sketch some plausible “double fusion” constructions - via delooping, quintet and Grothendieck approaches - briefly highlighting how these encode lattice-like structures, domain walls, and junctions between phases.
Composing "flavoured" Petri nets
David Jaz Myers
(Topos)
28th of August, 2025
We’ll describe a doctrine of various flavors of Petri nets in the double operadic theory of systems framework.
There is No Band: Double Categories, Fragmented Spacetime, and an AQFT
Khyathi Komalan
(California Institute of Technology)
21st of August, 2025
David Lynch’s neo-noir classic Mulholland Drive challenges our sense of continuity, identity, and causality. In this talk, I use its fragmented narrative structure as a metaphorical guide to construct an algebraic quantum field theory using a double functor between free globularly generated double categories.
We define a double category of spacetime regions where vertical morphisms are inclusions, horizontal morphisms are causal maps, and squares ensure compatibility between the two. On the algebra side, we use Juan Orendain’s double category of von Neumann algebras and bimodules using a general construction from decorated bicategories. The result is a functor that captures how observables evolve and embed across spacetime in a way that traditional approaches don’t cleanly separate. We discuss how gluing and locality can be modelled in this construction.
Along the way, we use the storyline of Mulholland Drive to guide our intuition and structure the talk — from fragments of time and overlapping realities to a new way of understanding gluing and locality in field theory. No background in physics is assumed — just curiosity, and a willingness to follow a story where not everything is what it seems.
Enriched categories applied to qualia spaces
Q Le
(University of Oxford)
7th of August, 2025
Recently, Tsuchiya and Saigo used Category Theory to formalise relationships between experiences [1]. In particular, they used Enriched Category Theory to model qualia structure based on similarity judgements, applying it to the case of colour similarity [2]. Within their paper and general work, they advocate for a certain view of categorical consciousness based on Yoneda’s Lemma, which could “characterise a quale as its relationship to all other qualia.” But is this right?
In this talk, we’ll consider and answer three core questions from their paper:
From the paper itself, “What kinds of relations (including similarity) can form an enriched category?”
Does their categorical approach work?
What are other applications of enriched category theory to consciousness?
[1] Tsuchiya, N. and Saigo, H. (2021) A relational approach to consciousness: categories of level and contents of consciousness. Neuroscience of consciousness. [Online] 2021 (2), niab034–niab034
[2] Tsuchiya, N., Phillips, S. and Saigo, H. (2022) ‘Enriched Category as a model of qualia structure based on similarity judgements’, Consciousness and Cognition. [Online] 101 (103319).
A modal proof of the Nerve Theorem
David Jaz Myers
(Topos)
24th of July, 2025
Joint work with Mitchel Riley.
The nerve theorem is a classical result in homotopy theory, usually attributed to Borsuk, which computes the homotopy type of a (paracompact) topological space from a “good” open cover of it. An open cover is “good” when finite intersections of opens in the cover are contractible whenever they contain a point; the nerve of a good open cover is the simplicial complex with a point for each open in the cover, and an -simplex for each inhabited intersection of opens in the cover. The nerve theorem states that the homotopy type of is the same as the nerve of any good open cover of it.
In this talk, we’ll prove the nerve theorem in the setting of modal homotopy type theory. The key concepts in the nerve theorem — the homotopy type of a space, the homotopy type presented by a simplicial set, and even the Čech nerve itself — may all be understood as “modalities” which act on simplicial, spatial homotopy types (that is, simplicial stacks on a suitably topological site). Once we understand the idea of modalities, we’ll see that the nerve theorem is a completely modal statement concerning the commutation of two sorts of “cohesion” possible for types (in Lawvere’s sense): the combinatorial cohesion of simplices, and the continuous cohesion of topology. As a result, we’ll actually be proving a nerve theorem for all spatial stacks in a direct, conceptual way.
The second (graphical) calculus of relations: Peirce’s Existential Graphs
Nathan Haydon 3rd of July, 2025
C.S. Peirce’s Existential Graphs are a precursor to string diagrams as we know them today. In this talk I’ll discuss the assumptions that led Peirce to develop the graphs and give an overview of how Peirce’s work inspired recent developments in categorical logic.
2-classifiers for 2-algebras
Matteo Capucci 26th of June, 2025
In this talk I will report on work in progress, joint with David Jaz Myers, about lifting discrete opfibration classifiers (2-classifiers, i.e. a ‘Set’-like object) from a 2-category K to the 2-category of algebras of a 2-monad T.
In the setting of DOTS, we often construct behaviour functors as ‘representables’, but without a 2-classifier one can’t really call these ‘representables’. Moreover, there is a strong connection between compositionality of such functors, the properties of the algebra they map out of, and the properties of the object(s) that represents them.
These phenomena are in fact completely general, so we set out to better understand the situation and found some frankly interesting notions and results, chiefly a tight result on the existence of 2-classifiers for 2-algebras.
Who cares about values?
B. Rousse
(Topos)
19th of June, 2025
Today it is common to hear about “human values” and the importance of designing technologies that “align” with our values. But where does this notion of “human values” come from? In this talk I trace the history of the concept of “human values.” I connect this notion with an evolution in our understanding of human autonomy, and argue that both are inadequate abstractions for the challenges of being human in our technological age. Finally, I introduce the notion of care as an alternative to “values,” showing how it furnishes a subtler map for imagining and shaping our relationship to technology today.
Double functorial representation of indexed monoidal structures
José Siqueira
(Topos)
12th of June, 2025
The data of a logical doctrine acts in two directions: that of the substitution operation, and that of quantification. Double Category Theory provides the tools to capture these two actions and their relationship concomitantly: in a double category of spans, re-indexing and acting on predicates can be packaged as tight and loose arrows respectively, and in there tight arrows always have conjoints. By mapping these conjoints into a double category of quintets, we obtain adjunctions internal to a 2-category. Moreover, by using the notion of adequate triple, the indexing category need only have certain pullbacks.
Adding a monoidal structure to the fibers (and the double pseudofunctor) allows us to capture both the Beck-Chevalley and Frobenius conditions. We will concern ourselves with the monoidal analogues of regular hyperdoctrines and similar structures (where the objects of predicates are not necessarily posets, but rather live in some 2-category), and show how they are equivalent to (lax symmetric monoidal) double pseudofunctors between spans and quintet double categories.
AI for precision oncology
Elizabeth Amelia
(Imperial College London)
29th of May, 2025
This talk centers around the design and implementation of robust, end-to-end machine-learning pipelines for predicting patient response from high-dimensional molecular data. We’ll walk through each critical stage—data ingestion and normalization, leakage-proof nested cross-validation, stability-based feature selection to derive reproducible biomarker panels, hyperparameter optimization, calibration of probability outputs, and external cohort validation—highlighting why every step matters for building reliable, generalisable models.
Advancing human-machine interface systems through artificial intelligence
Samuel George-White
(Imperial College London)
22nd of May, 2025
This study explores the use of artificial intelligence to improve human–machine interaction by decoding neural intent from non-invasive muscle signals. Using a GO/NO-GO task, we recorded high-density electromyography (HD-EMG) and EEG data from participants during movement preparation and cancellation. After preprocessing the data — including filtering, dimensionality reduction (PCA), and normalization — we trained a convolutional neural network to classify different movement-related brain states. The model achieved 72.4% accuracy in distinguishing two functional states and 49.6% in three-class classification. Visualization techniques such as GradCAM and temporal sliding windows were used to interpret model decisions and understand how neural signals evolve over time. These findings highlight the potential of using surface EMG to decode brain activity, paving the way for more intuitive control in applications like prosthetics, rehabilitation, and real-time assistive technologies.
Diagrammatic Equations
Tim Hosgood
(Topos)
15th of May, 2025
This talk will be a repeat of a previous talk (sorry!) on expressing equations — differential, linear recurrence, hidden Markov model, … — using the language of diagrams in categories. We will see some examples arising from multi-physics and understand how this formalism is useful for modellers.
Developing programming language support for end-to-end verification of neural AI agents
Matthew Daggitt 1st of May, 2025
Over the past decade, there has been impressive progress in developing algorithms capable of formally verifying first-order, linear specifications about small-to-medium-sized neural networks. This has opened the door to formally verifying the correctness of neural AI agents operating in complex environments. However, due to the complexity of integrating these verification algorithms with other reasoning tools and the many moving parts involved, deploying them in practice has proven more challenging than anticipated.
In this talk, I will introduce Vehicle, a tool that my collaborators and I have been developing. Vehicle allows users to:
write specifications for AI agents in a high-level, domain-specific language;
use these specifications to guide training;
formally verify whether the resulting neural network satisfies the specification; and
export verified specifications to interactive theorem provers where the agents can be reasoned in the context of their environment.
In the talk I will highlight how we leverage type theory in unusual ways to improve the user experience, our use of real-valued logic semantics to interpret Boolean specifications, and finally some of the open theoretical challenges in the field.
The Path-Complete Formalism for Switched Systems: Stability and Beyond
Virginie Debauche
(Oxford University)
17th of April, 2025
Switched systems play a crucial role in modern engineering thanks to their ability to capture complex behaviours involving transitions between different operational modes. However, analyzing their stability remains a challenging task due to the intricate interplay between discrete switching and dynamics. This complexity calls for sophisticated mathematical tools. While Lyapunov theory remains a cornerstone of stability analysis, traditional methods often fall short when applied to switched systems, prompting ongoing efforts to extend the theory to better accommodate their unique characteristics.
This talk presents the framework of path-complete Lyapunov functions, which offers a fresh perspective by integrating combinatorial structures to represent switching behaviour. Specifically, a path-complete Lyapunov function comprises two components: a combinatorial element, represented by an automaton (a directed graph) that encodes admissible switching sequences, and an algebraic element, consisting of a collection of Lyapunov functions—one for each node in the graph. The graph edges govern how these Lyapunov pieces interact and decrease across transitions. This framework is particularly appealing for the analysis of switched systems because it allows for the construction of tailored, nonstandard, and less conservative stability criteria, all while mitigating the combinatorial complexity that often burdens classical optimization techniques.
While originally introduced for stability analysis, the path-complete Lyapunov framework has been recently extended to encompass constrained switching systems, stabilization via switching sequence and control Lyapunov function design, and safety through path-complete barrier functions. This talk will highlight these recent developments and their unifying role within the framework.
Physiologically-based demographic modelling
George Simmons
(IDEMS)
15th of April, 2025
Representability of reachability problems in algebras for double operads
David Jaz Myers
(Topos)
3rd of April, 2025
Everettian quantum mechanics and the problem of ontological extravagance
Rachel Pedersen
(Oxford University)
27th of March, 2025
Since it neither relies on a collapse postulate nor posits a hidden variable, Everettian quantum mechanics (EQM) is an attractive option among realist interpretations of quantum mechanics. In some sense, EQM is a simpler theory than its competitors. However, it also appears to require more structure; unlike its competitor theories, EQM has traditionally been taken to entail a multitude of worlds, as every possible outcome of every quantum process is actualized in at least one world. Since no other realist competitor theory shares this feature, the most prominent objection raised against EQM is that of ontological extravagance.
Everettians have given this objection little serious attention, at least in part because the objection from ontological extravagance has not yet been carefully articulated in the literature. To clarify this objection, I distinguish between two types of simplicity criteria: ones concerned with ontological abundance and others concerned with postulate abundance. Where ontological abundance criteria concern the number of concrete objects that some theory posits, postulate abundance norms instead concern the number and overall complexity of the set of postulates of the theory. Unfortunately, it is unclear how we ought to weigh these simplicity-related metaphysical considerations, and worse, as I argue, there is no independent motivation for either sort. I argue that we ought to instead consider the proximity between the way the theory says the world is, and the way the world appears to be. With the deadlock between Everettians and non-Everettians on what sort of simplicity criterion reigns supreme, this severely overlooked criterion offers a promising route forward in the dialectic. This alternate criterion roughly corresponds to what Emery (2023) calls the minimal divergence norm, under which we ought to prefer theories that deviate least from the manifest image, or the way the world generally appears to be. However, such a norm requires further specification; there is no image of the world that uniquely picks out the manifest image. Observations themselves depend on our theoretical commitments, which vary from agent to agent, and so there are many manifest images. To avoid this multiplicity, I argue that we ought to look to the physical sciences for a widely-accepted theory that describes the world as we experience it. Classical mechanics (CM), the predecessor theory to quantum mechanics, does exactly that; though it is certainly not a correct description of reality, it is sufficiently accurate for numerous forms of engineering, as it describes macroscopic reality well enough. I argue that we ought to treat the way that classical mechanics says the world is as the manifest image. Then, the third type of criteria, which I call classical divergence, concerns the degree to which the way some theory in question says the world is deviates from the way that CM says the world is. I defend this norm on pragmatic grounds, arguing that adhering to it offers a distinct epistemic advantage.
While EQM does not necessarily tell us that our world is vastly different from the way that CM says it is, it is generally taken to entail many more worlds than its competitor theories. With this new set of simplicity criteria in place, Everettians can better understand the available dimensions along which they may endeavor to improve their ontology. This new norm that I advocate offers hope: Everettians can seek a less extravagant ontology by strategically minimizing classical divergence.
Open translations in mathematics
Tim Hosgood
(Topos)
20th of March, 2025
Translation, in full generality, is a nuanced and complex art form that requires serious expertise and a holistic approach. So how can we as mathematicians hope to “solve the problem of translation” in our domain? Furthermore, can we do so without making access to academia even harder for non-native English speakers or hurrying a domain collapse of non-English languages? I believe that the answer to both of these questions can only possibly be “yes” if we approach translation as a community-driven activity. In this talk, I will speak about my experiences in working on large translation projects with an open-source approach — the technology and methodology that was helpful for doing so, as well as some of the difficulties — and describe the sorts of resources that I believe would have been helpful. Hopefully this can form a starting point for community thought on the types of projects that we could focus on in the future. (This talk is a repeat of a talk given recently at the Isaac Newton Institute).
Neural certificates
Mirco Giacobbe
(University of Birmingham)
13th of March, 2025
Model checking aims to derive rigorous proofs for the correctness of systems and has traditionally relied on symbolic reasoning methods. In this talk, I will argue that model checking can also be effectively addressed using machine learning too. I will present a realm of approaches for formal verification that leverage neural networks to represent correctness certificates of systems, known as “neural certificates.” This approach trains certificates from synthetic executions of the system and then validates them using symbolic reasoning techniques. Building upon the observation that checking a correctness certificate is much simpler than finding one, and that neural networks are an appropriate representation for such certificates, this results in a machine learning approach to model checking that is entirely unsupervised, formally sound, and practically effective. I will demonstrate the principles and experimental results of this approach in safety assurance of software, probabilistic systems, and control.
Element Model Type Theory
Owen Lynch
(Topos)
6th of March, 2025
Generalized algebraic theories have long been part of our work at Topos, going back to the very beginnings of Catlab.jl. In this talk, I give a new implementation of generalized algebraic theories in Rust, which takes a different, more type-theoretic approach to generalized algebraic theories. This approach tightly integrates e-graphs into the type-checking process to enable an approximation to extensive equality, and in addition enables greater compositionality of theories, achieving a principled approach to “theory pushout” that has been long-desired. This new implementation is intended as a prototype for type-checking algorithms that will go into CatColab and enable “open notebooks” for compositional modeling, and I give an overview of how I envision that working. In addition to this application in scientific modeling, I believe that lessons from this implementation that I have learned about two-level type theory could be applicable in a wide variety of domains in which abstraction is desired that does not complicate the underlying semantics, such as finite state machines, probabilistic programming, SAT solving, systems programming, constraint programming, databases, and serialization formats.
A next-generation modular and compositional framework for System Dynamics modeling and beyond
Xiaoyan Li
(Topos)
27th of February, 2025
System Dynamics (SD) is a powerful methodology for understanding and managing complex systems over time, with applications in various fields such as public health, business, and environmental management. Despite its strengths, traditional System Dynamics modeling methods face several critical limitations, including a lack of modularity, inadequate representation of complex relationships, stratification that obscures model transparency, rigid coupling of model syntax and semantics, and limited support for model composition and reuse. These challenges restrict the scalability, adaptability, and accuracy of models, particularly when applied to large-scale or interdisciplinary systems.
To address these limitations, this presentation introduces a novel framework grounded in Applied Category Theory (ACT), which provides a rigorous mathematical foundation for representing, relating, composing, and stratifying complex systems. By leveraging ACT, this research establishes a next-generation SD modeling approach that integrates mathematical rigor with practical utility, significantly enhancing the flexibility, expressiveness, and applicability of System Dynamics for researchers and practitioners across various domains.
To contextualize System Dynamics modeling in the realm of infectious disease simulation, the presentation will begin with an overview of a COVID-19 theory-based machine learning model, developed incorporating the Bayesian methodology of Particle Filtering algorithm to a Covid-19 System Dynamics model. This model played a pivotal role in supporting decision-making across 17 Canadian jurisdictions during the COVID-19 pandemic by providing daily transmission monitoring, short-term projections, and counterfactual intervention analysis over a year.
Charles Peirce, inference, and category theory
David Corfield
(University of Kent)
20th of February, 2025
The American philosopher Charles Saunders Peirce (1839-1914) had much to say about the nature of intellectual enquiry. In the realm of deductive logic, category theorists have made important use of his string-diagrammatic logical calculus. But Peirce’s interests in inference extended beyond deduction to induction and abduction. In this talk I shall be exploring the thesis that we can understand this triple in terms of the category-theoretic notions of composition, extension and lift. We will also touch on his broader semiotics and his account of concept formation.
Markov semigroups
Owen Lynch
(Topos)
14th of February, 2025
This talk covers the basics of Markov semigroups from a slightly categorical point of view, with an aim of conveying a basic intuition about the setup for and the meaning of the Hille-Yosida theorem. At the end, a synthetic viewpoint is conjectured.
What 2-algebraic structure do cartesian pseudo-functors preserve?
David Jaz Myers
(Topos)
31st of January, 2025
If universal algebra is the study of sets equipped with the structure of some operations satisfying universally quantified equations, then 2-algebra is the study of categories equipped with the structure of some operations, some natural transformations between these operations, and some equations between these. Examples of 2-algebras include symmetric monoidal categories and categories with finite products.
Just as the functorial semantics (due to Lawvere) for algebra lets us interpret algebraic theories in categories other than sets (so long as they have finite products), the functorial semantics for 2-algebra (due to Power, Lack, and others) lets us interpret 2-algebraic structure in 2-categories other than Cat. For example, instead of symmetric monoidal categories, we can consider symmetric monoidal double categories.
Any strict 2-functor that preserves finite products will push forward 2-algebraic structure. But 2-functors are often only functorial up to coherent isomorphism. What 2-algebraic structure do such cartesian pseudo-functors preserve? In this talk, we’ll ask the question and put forward an answer: so long as the 2-algebraic theory is flexible, in the sense that it only asks for equations between transformations and not between operations, then it will be preserved by cartesian pseudo-functors.