We introduce the delayed stabilizer ZX-calculus, a formal graphical language for translation-invariant stabilizer quantum processes: enabling compact, finite reasoning about various families of infinite stabilizer-codes, such as quantum convolutional codes and lattice codes. Our calculus extends the odd-prime-dimensional stabilizer ZX-calculus with only a single additional generator, the delay, which feeds data from one time step to the next.
First, we give an interpretation of delayed ZX-diagrams as sequences of finite approximations obtained by unrolling the diagram in time. We define a notion of observational equivalence between such sequences and prove that, modulo this equivalence relation, each sequence determines a unique infinite-dimensional stabilizer group.
Second, we interpret the delay as multiplication by a formal polynomial indeterminate, encoding infinite sequences of Pauli operators as fractions of polynomials. This allows us to represent the infinite stabilizer group of a delayed stabilizer circuit in terms of a finite generating tableau. We connect both semantics via geometric-series expansion, showing that composition in the infinite stabilizer group semantics approximates composition in the generating tableau semantics.
Finally, we give an equational theory for delayed stabilizer ZX-calculus, featuring generalised Euler decomposition and colour change rules. We show that this calculus is sound and universal for the generating tableau semantics. Combining delayed ZX-calculus with scalable notation, we present a novel generalised local complementation rule for translation-invariant graph state. We conjecture that this rule follows from the axioms of our calculus, from which completeness would follow.
ZX Sketch (https://zxsketch.com) is a free, browser-based graphical editor for the ZX calculus, a graphical language whose diagrams are morphisms in a prop and whose rewrite rules provide a complete axiomatisation of qubit quantum mechanics. Users draw and manipulate ZX diagrams directly in the browser with no installation required, applying rewrites through intuitive gestures: spider fusion is dragging two spiders together, color change is a double-tap, and the Hopf rule is cutting two parallel wires.
ZX Sketch features 19 interactive rewrite rules with pattern matching and one-click application, 18 automated simplification strategies, and a proof mode with step-by-step timeline navigation, goal diagrams, and tensor verification, all powered by PyZX running in-browser via Pyodide and WebAssembly. Soundness of every rewrite is guaranteed by delegation to PyZX; the tool will never apply an unsound rewrite. Export is supported to TikZ, SVG, PNG, PyZX JSON, and URL-based sharing, with full ZXLive interoperability.
Taking inspiration from ZXLive's interactive rewriting model and the interaction design of Desmos, ZX Sketch aims to make the ZX calculus accessible to newcomers and educators. We are developing a progressive tutorial mode inspired by Kontorovich's Real Analysis Game, guiding users through the sound rewrite rules of the ZX calculus incrementally toward completeness. During the demonstration, we will invite attendees to follow along on their own devices at zxsketch.com.
Source code: https://github.com/hstoltz/ZX-sketch (Apache 2.0, DOI: 10.5281/zenodo.18841742)
Sequential Monte Carlo (SMC) algorithms, also called particle filters, were developed for approximate inference in state-space models. They maintain a population of weighted samples, called particles, that are periodically resampled to prevent weight degeneracy. More broadly, SMC applies whenever a target distribution can be decomposed into a sequence of intermediate steps. Traditionally, these algorithms are formalized using discrete-time Feynman-Kac models which consist of a sequence of Markov kernels and potential functions.
In this talk, we interpret SMC categorically: any string diagram of s-finite kernels gives rise to a weighted particle sampling scheme. This extends the string-diagrammatic account of exact filtering given by Fritz et. al. 2025. We establish correctness by deriving a law of large numbers from compositional stability properties. Finally, we describe how this framework has guided the design of probabilistic programming languages in Julia and PyTorch and enables intuitive reasoning about programs.
Category theory has seen a rise in applications in deep learning, bringing with it ideas and tools from functional programming and dependent type theory. However, practical implementations of these ideas face significant friction. Successful neural network frameworks only exist in dynamically typed languages such as Python, and attempts to implement these ideas in statically-typed languages have struggled with expressiveness and ergonomics, typically only replicating what exists without imagining what can be.
In this talk, I will introduce TensorType, a tensor processing framework implemented in Idris 2 aiming to demonstrate that ergonomics and rigor need not be at odds. TensorType provides tensor operations checked at compile-time while enabling fundamentally new capabilities: tensors that branch and recurse instead of being confined to rectangular shapes. I will walk through the design choices behind TensorType, showcase how containers power its core abstractions, and explore strange new worlds it enables.
Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We present a categorical framework for assume-guarantee reasoning for safety problems by viewing systems as \emph{lenses}, following our earlier work on the compositionality of generalized Moore machines. Generalized Moore machines include ordinary Moore machines, partially observable Markov (decision) processes, and systems of parameterized ODEs (control systems); our framework gives assume-guarantee reasoning specially adapted to each of these cases. In particular, we give a novel formulation of assume-guarantee reasoning for \emph{(local) input-to-state stability} ((L)ISS) Lyapunov functions on systems of parameterized ODEs.
Our framework is categorically natural and straightforwardly compositional. A flavor of generalized Moore machine is determined by a \emph{tangency}: a fibration with a section. We show that symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be constructed 2-functorially from fibrations internal to the 2-category of tangencies.
Regulatory documents are not organized as isolated rules, but as interconnected systems of provisions, definitions, exceptions, and cross-references. Modeling explicit logical structure, including relevance, dependency, and order of evaluation, can help organize regulatory documents for computation across multiple levels of applicability and evaluation. In this paper, we propose a three-layer category-theoretic model for regulatory documents: a versioning layer, a layer of document structure and rule traversal, and a layer of local rule semantics. The latter two are organized as set-indexed families of categories. This framework gives a knowledge representation of regulatory documents using Spivak and Kent's ontology logs (ologs) [1] that supports structured reasoning. We illustrate the three-layer framework in the setting of building codes to demonstrate how these layers can be instantiated in a concrete regulatory domain.
[1] David I. Spivak and Robert E. Kent. Ologs: A categorical framework for knowledge representation. PLOS ONE, 7(1):1–1, 01 2012.
We are interested in control problems with hidden state, where one system must interact with another in order to keep their combined state within some predefined set of "good" states. In such a setting it is natural to ask questions like "what does the controller know about the state of its environment?". In previous work [1] we showed how to make such questions formal, modelling controller X and environment Y as Moore and Mealy machines respectively. We have shown that under minimal hypotheses any successful controller admits a "semantic" map to the set PY of subsets of the state space of the environment, thought of as "beliefs", and that this map commutes with a dynamics given by "possibilistic Bayesian conditioning".
Here we show that PY, together with the possibilistic updating procedure, generalises to a system (in the sense of categorical systems theory) with the universal property of a power object with respect to a suitable fibration of predicates. Specifically, we model behaviour of machines in the so-called behavioural doctrine, where we can study 'behaviours of systems' displayed over 'behaviours of their interface'. By choosing a suitable fibration of 'forward-closed predicates' we can express the relevant concepts from control theory. We observe that products of behaviours over a fixed interface are an expressive enough kind of coupling, and thus the universal property of a power object says that predicates over coupled behaviours X ⨉_I Y are in bijection with maps X → PY. These maps take on the role of the map from states of the controller to beliefs about its environment, which gives some insight into why we should expect such semantic interpretations to exist in a control theoretic setting: the agent's ability to perform the task and the map from its states to beliefs are, in this precise sense, the same thing. We focus on two rich exemplar settings, behavioural theories valued in presheaf toposes, and those valued in (small, strict) categories. We show that the dynamics of PY correspond to possibilistic belief updating in a very intuitive way.
[1] Virgo, Biehl, Baltieri, Capucci (2025) A "good regulator theorem" for embodied agents. In Proceedings of Artificial Life 2025, https://doi.org/10.1162/ISAL.a.874
The category of polynomial endofunctors and natural transformations, equivalently known as the category of containers and dependent lenses, is well known to have a wide variety of potential applications. We will demonstrate Polylang, a high level programming language and compiler designed to support all of these applications while being agnostic between them. From a theoretical perspective it is an implementation of the intrinsic simple type theory of $\mathbf{Poly}$: its types denote polynomials and its functions denote lenses, and as such have a "forwards pass" and a "backwards pass".
The operator basis supported by Polylang includes the cartesisan product, tensor product, coproduct, composition product and fixpoints. The interaction of cartesian and tensor products requires a system of quantities inspired by graded and quantitative type theories. The composition product is the most difficult to include since it resists straightforward implementation in a natural deduction calculus, but we achieve it with an imperative style language via a sequent calculus exploiting the isomix linearly distributive structure. Algebraic datatypes involve fixpoints of polynomial endofunctors on $\mathbf{Poly}$ itself, and significantly increase expressive power, including allowing the embedding of various categories of traversals as kleisli categories of definable monads.
The plan for the talk is to explain some of this theory in the syntax of the language itself while also demonstrating the compiler in action.
The category Poly, of polynomial endofunctors on Set, is known to have a rich array of categorical structures and has featured extensively in work on applied category theory. The perspective of Poly’s morphisms as bidirectional transformations leads to them being a useful model for processes following a request/response pattern, with a covariant component propagating requests and a contravariant part returning responses, whose types are dependent over their correspondent requests. Polynomial functors are closed under composition, acting as a kind of sequencing operation, interleaving requests and responses into more complex interaction patterns. While this can be a powerful semantic domain for modelling interactive systems, notations for defining polynomials and their morphisms can be combersome in complex situations, obfuscating the underlying information flow being expressed. This work aims to find a suitable language for defining polynomials and their morphisms in an ergonomic fashion.
Von Glehn (2014) showed how Poly can be used as a model of intuitionistic dependent type theory (ITT), however the structural nature of intuitionistic type theory means that many of the features that make Poly interesting as a category of study are inaccessible within this syntactic presentation. In particular the bidirectional nature of morphisms in Poly is obfuscated, with much of the logical structure merely reflecting that of the base category, Set. We explore a selection of extensions to dependent type theory with Poly as an intended model, which allow for practical axiomatisations of more specialised structures in Poly.
Extending ITT with a pair of adjoint modalities, related to those of spatial type theory, facilitates the definition of “response types” which provide a way for types to refer to the contravariant component of polynomials, and lead to introduction and elimination rules for the composition product of polynomial functors, related to the semantics of algebraic effects systems.
We then consider a graded linear theory in which contexts are modelled by a dependent version of the Dirichlet product of polynomials. This system functions similarly to other linear dependent type theories where a distinction between term-level usage and type-level usage is mediated by a notion of ‘erasure’, such as that in Quantitative Type Theory of Atkey (2018). We find that a modified form of erasure, which we refer to as ‘coerasure’, has a natural interpretation in Poly as the comonadic modality in our previous system.
Finally we show how Poly can be used as a model for a bunched dependent type theory similar to the bunched theory for parameterised spectra of Riley (2022). In contrast to the models which Riley considers, polynomials model type dependency in a more restricted fashion, allowing us to simplify some of the details of Riley’s system while still providing a powerful language for manipulating morphisms of Poly.
We present a compositional framework for nature derived material design using applied category theory, together with a computational implementation that makes the construction executable. Bioinspired design is often carried out by informal analogy: a biological mechanism is identified, translated into an engineered material or geometry, and then revalidated at each scale of assembly. This becomes difficult to manage when the target behavior emerges from multiscale organization. To address this, we define a category Dyn of stimulus response systems, whose objects are dynamical systems with environmental input and whose morphisms satisfy a simulation condition. Biological and engineered systems are modeled as subcategories Nat and Art of Dyn. An implementation functor F: Nat -> Art maps natural hierarchies to engineered ones while preserving their interscale structure, so that interface consistency is enforced compositionally rather than rebuilt case by case.
To connect behavioral models to realization, we introduce a category Spec of fabrication specifications together with a semantic projection pi: Spec -> Art and an execution map from Spec to machine level programs. This separates behavioral correctness from hardware specific execution and yields a computational pipeline in which multiscale objects, assembly maps, reductions, and implementation maps are encoded explicitly and checked at their interfaces. In our implementation, the categorical hierarchy is instantiated as an executable design workflow that supports parameterized model construction, generation of engineered variants, and translation to fabrication ready artifacts. The central claim is a compositional verification principle: once local interface conditions are verified, system level validity follows by composition, and computational realizations that preserve the same semantics can be refined without changing the verified behavioral target. We instantiate the framework on a multiscale hygromorphic pinecone model and show how the same formal and computational pipeline generates engineered designs across distinct stimulus response pairings. The contribution is therefore a categorical and executable account of multiscale translation, verification, and fabrication for materially embodied design.
Website based on a bootstrap design by Hartmut Eilers and Eric Koskinen.