Categories, Logic, and Physics, Scotland

CLAP Scotland is a forum for applications of category theory and logic to physics and computer science, that aims to maintain and enhance the cohesion of Scottish research in these areas. The meetings provide an informal atmosphere where participants can easily interact. They are open, and all are welcome to attend, in particular research students. This is a continuation of the series of CLAP workshops in the greater London area held biannually 2008-2010, and of the Scottish Category Theory seminar that ran biannually 2009-2014, and we encourage the same friendly and open atmosphere. If you would like to host a meeting or give a talk, contact Chris Heunen.

Third meeting: Wednesday 5 April 2017

The third meeting will be held on 5 April 2017, in the Department of Computer and Information Sciences at the University of Strathclyde, in room 1415 of Livingston Tower.


  • 10:00: Coffee
  • 10:30: Kevin Dunne (University of Strathclyde): Infinite-Dimensional Categorical Quantum Mechanics, Spectra, and Contextuality
    There have been several projects reformulating some aspect of quantum theory in the language of category theory, for example: the monoidal approach to quantum theory, which encodes aspects of quantum theory as algebras internal to some symmetric monoidal category (e.g. Frobenius, Hopf, or H*-algebras); the topos approach of Butterfield, Isham and Doering, which embeds traditional quantum theory into a the framework of topos theory; and an approach to quantum logic of Heunen and Jacobs based on the semilattice structures associated with dagger-kernel categories.

    These three approaches are independent of one another, however we show an interaction between them. The combined approach embeds the monoidal approach into a topos framework, and with the addition of dagger-kernels we can derive structure theorems for Frobenius algebras and H*-algebras. Analogous to studying groups by considering their linear representations, we give a canonical representation theory for the kinds of internal algebras typically studied in the monoidal approach to quantum theory. We can then use these structure theorems to address the question of whether or not a category exhibits contextuality, in particular we obtain a proof that the category of sets and relations is non-contextual.
  • 11:10: Chris Heunen (University of Edinburgh): The category of Hilbert modules
    Categorical quantum mechanics abstracts away from Hilbert spaces to see how much of quantum theory can be given a conceptual categorical basis. Nevertheless, the main examples remain based on Hilbert spaces or sets and relations. In particular, the scalars are usually thought of as numbers. I will discuss the category of Hilbert modules, where the scalars hide the structure an underlying space(time). The objects may be regarded as state spaces that vary continuously over a base space(time). Hence the category may be regarded as capturing a naive quantum field theory rather than quantum mechanics. I will analyse the Frobenius structures in this category and give nontrivial infinite-dimensional examples. I will also discuss localisation: open subsets of the base space correspond to idempotent subobjects of the tensor unit. Finally, I will discuss work in progress about applying these techniques to categorify relativistic quantum information theory.
  • 11:50: Fabio Zanasi (University College London): A new foundation for string diagram rewriting: adequacy, confluence, commutativity
    String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. In this work we give a sound and complete interpretation for this form of rewriting in terms of double pushout (DPO) rewriting of hypergraphs, subject to a convexity condition. Non-convex rewriting in this domain is also interesting, as syntactically it corresponds to rewriting modulo a chosen separable Frobenius structure. Time permitting, two further results strengthening this approach will be shown. The first is that, contrary to arbitrary hypergraph rewriting, with our setup confluence becomes decidable for terminating rewriting systems. The second is a sound and complete interpretation of commutative operators as additional Frobenius structures, which addresses the problem of non-termination of commutativity as a rewrite rule.
  • 12:30: Lunch
  • 14:00: Aleks Kissinger (Radboud University): A categorical semantics for causal structure
    I'll present a categorical construction for modelling both definite and indefinite causal structures within a general class of process theories that include classical probability theory and quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode finegrained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. I'll give several examples, including non-signalling processes, quantum n-combs, and OCB process matrices and show how the operational behaviour of such processes can be derived from the categorical structure.
  • 14:40: Stefano Gogioso (University of Oxford): Infinite-dimensional Categorical Quantum Mechanics
    I will present some recent developments in the non-standard framework for infinite-dimensional categorical quantum mechanics. I will start by introducing the category Star Hilb, which is dagger compact and comes with unital dagger Frobenius algebras. I will provide explicit constructions for the Hilbert spaces of wavefunctions in boxes with periodic boundary conditions, wavefunctions on lattices, and wavefunctions in real space. Time permitting, I will also sketch a couple of constructions of interest in quantum field theory.
  • 15:20: Tea
  • 15:40: Peter Hines (University of York): Diagrams and Coherence Theorems in Cryptography and Cryptanalysis
    This talk intends to demonstrate that categorical diagrams are a simple and convenient way of visualising and reasoning about cryptographic protocols. We illustrate this with various examples of both popular and obscure protocols, to demonstrate how the flow of information among the participants may be modelled. We also provide evidence for the claim that there are deeper connections between category theory, complexity, and cryptography than simply modelling information flow.

    The talk is very much aimed at category theorists who are interested in how their field may be applied to cryptography, rather than vice versa. No prior knowledge of cryptography is required, but some category-theoretic background will be assumed!
  • 16:20: Clemens Kupke (University of Strathclyde) Games for topological fixpoint logics
    Topological fixpoint logics are logics that are interpreted over topological models and where the fixpoint operators are defined with respect to these topological interpretations. In my talk I will discuss a variant of these logics for relational structures based on Stone spaces, where the fixpoint operators are interpreted via clopen sets. I will present a game-theoretic semantics for this logic. The adequacy and bisimulation-invariance of this semantics will be the main technical results of my talk.

    The motivation for this work is two-fold: i) studying topological models of modal fixpoint logics might shed new light on completeness proofs for these logics and ii) restricting the interpretation of formulas to so-called admissible subsets of the model adjusts the expressiveness of the logic to capture natural topological properties of the model (e.g. reachability-in-the-limit as opposed to standard reachability).
  • 17:00: Pub

Registration is free, but for catering purposes please email the local organiser Ross Duncan as soon as possible if you plan to attend.

You might also be interested in the workshop on Algebra and Coalgebra meet Proof Theory held at the University of Strathclyde on April 10-12.

Second meeting: Wednesday 30 November 2016

The second meeting was held on 30 November 2016, in the Department of Computer and Information Sciences at the University of Strathclyde, in room 1415 of Livingston Tower.


  • 10:00: Coffee
  • 10:30: Ulrich Kraehmer (University of Glasgow): What is a quantum symmetry?
    Since the 1980s, algebraists studied quantum groups (Hopf algebras) as generalised symmetries, and they extended various concepts and results from group theory to quantum groups. After giving a small survey of this story, I will explain a paper with Angela Tabiri in which we show that planar curves have way more quantum symmetries than classical ones, and also more than we expected. [slides]
  • 11:15: Kevin Dunne (University of Strathclyde): Endomorphism semialgebras in categorical quantum mechanics
    The category Rel of sets and relations has been studied extensively from the perspective of the monoidal approach to quantum theory. Here we take a look at Rel from the perspective of the topos approach to quantum theory. To do this we must generalise aspects of the topos approach to quantum theory, in particular we generalise C*-algebras and their Gelfand spectrum, which we do using the language of semialgebras. We will then compare this perspective of Rel to that of the monoidal approach to quantum theory, and see a surprisingly similar picture emerge to that of the category of finite dimensional Hilbert spaces. [slides]
  • 12:00: Martti Karvonen (University of Edinburgh): Dagger categories: monads and limits
    A dagger category is a category equipped with a dagger: a contravariant involutive identity-on-objects endofunctor. Such categories are used to model quantum computing and reversible computing, amongst others. The philosophy when working with dagger categories is that all structure in sight should cooperate with the dagger. This causes dagger category theory to differ in many ways from ordinary category theory. Standard theorems have dagger analogues once one figures out what "cooperation with the dagger" means for each concept, but often this is not just an application of formal 2-categorical machinery or a passage to (co)free dagger categories. We will discuss two instances.
    First, as soon as a monad on a dagger category satisfies the Frobenius law, everything works as it should. Dagger adjunctions give riseto such monads. Conversely, such monads factor as dagger adjunctions in two canonical ways; however, the Eilenberg-Moore category needs to be adapted t o inherit the dagger.
    Second, limits in dagger categories should be unique up to an unique unitary, that is, an isomorphism whose inverse is its dagger. We rework an initial attempt to a more elegant and general theory. It works well when the diagram has a dagger; however, the formulation of limits using adjunctions needs to be adapted. We will discuss work on defining dagger limits of general diagrams.
    Finally, we will discuss formally how dagger categories, while perhaps slightly evil, are not all that bad. [slides]
  • 12:45: Lunch
  • 14:15: Tarmo Uustalu (Tallinn University of Technology): Grading monads, comonads and distributive laws
    We are accustomed to using strong monads to organize effectful computations in programming language semantics and monoidal comonads in a similar vein to organize coeffectful computations. I will show how a quantitative aspect can be added by grading, leading to mathematization of the old idea of effect systems from program analysis. I will first introduce graded (strong) monads, outlining both their theory and programming language applications, and will then discuss graded monads of monoids, graded distributive laws of a monad over a monad, graded (monoidal) comonads and distributive laws of a comonad over a monad.
    This is based on recent works by Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès, Flavien Breuvart, Marco Gaboardi, Dominic Orchard and myself. [slides]
  • 15:00: Dan Marsden (University of Oxford): Custom hypergraph categories via generalized relations
    Compact closed and hypergraph categories have become standard settings for work in categorical quantum mechanics, linguistics and general process theories. More recently, our group in Oxford has been looking at further applications in areas such as cognition. With each new application area, there is a need to identify a suitable category modelling thppe phenomena under consideration. In this talk we will describe a framework derived from generalized notions of relations, in which we can construct hypergraph categories which can capture features such as convexity, proof relevance, metrics and semantics varying with time or context. The framework is parameterized along 4 natural axes of variation, allowing users to flexibly configure hypergraph categories to their application needs. [slides]
  • 15:45: Tom Avery (University of Edinburgh): Notions of algebraic theory
    Intuitively, an algebraic theory is a kind of mathematical structure defined by some operations with various arities, that satisfy certain equations. There are lots of categorical ways of making this precise at various levels of generality, including monads, Lawvere theories, PROPs, monoids, and monads with arities. I will describe a notion of algebraic theory that specialises to each of these, and discuss some results that can be proved even at this very high level of generality.
  • 16:30: Tea and discussion

Registration is free, but for catering purposes please email the local organiser Ross Duncan as soon as possible if you plan to attend.

You might also be interested in the workshop on coalgebra, Horn clause logic programming and types held at the University of Edinburgh on November 28 and 29.

First meeting: Thursday 14 April 2016

The first meeting was held on 14 April 2016, in the School of Informatics at the University of Edinburgh, room G.07.


  • 10:30: Coffee
  • 11:00: Stefano Gogioso (University of Oxford): Fully graphical treatment of the Hidden Subgroup Problem
    The Hidden Subgroup Problem (HSP) encompasses several more specific problems of interest in quantum computation. Integer factorisation and the discrete logarithm are both special cases of the abelian HSP, while the graph isomorphism problem is a special case of the (yet-to-be-solved) non-abelian HSP. Today, we present the first fully-graphical treatment of the quantum algorithm for the abelian HSP. We highlight the key role played by strongly complementary observables in its formulation, and we investigate the extent to which they could be used to tackle the non-abelian HSP. [video]
  • 11:40: Sean Tull (University of Oxford): Operational physics, logic and categories
    Recent years have seen several reconstructions of quantum theory from among more general operational theories of physics, defined in terms of systems and probabilistic experiments one may perform upon them. A major example is the framework of 'operational-probabilistic theories' due to Chiribella, D'Ariano and Perinotti. I will introduce a close variant of these operational theories and show how they can be treated in an entirely categorical way, using the new notion of an operational category. Our approach comes from effectus theory, an area of categorical logic due to Jacobs, which we offer a new operational interpretation. This perspective also establishes interesting connections between the programmes of general probabilistic theories and categorical quantum mechanics. [slides] [video]
  • 12:20: Sander Uijlen (Radboud University): Indefinite causal structures using diagrammatic methods
    If we abandon the idea of a fixed causal structure and use local quantum mechanics, we can obtain probability distributions which are incompatible with even convex mixtures of causal structures. In this talk we take a look at some preliminary results of an investigation of these indefinite causal structures using diagrammatic methods. [slides] [video]
  • 13:00: Lunch
  • 14:00: Nick Behr (University of Edinburgh): Graph rewriting and combinatorial Hopf algebra
    A novel formulation of graph rewriting will be presented, the so-called rule algebraic formalism. Its mathematical foundation lies in the concept of a certain combinatorial Hopf algebra, namely the algebra of compositions of rule diagrams. The algebras of graph rewriting in its four different variants may be obtained in the form of reductions of the rule diagram algebra. Remarkably, the definition and study of the algebras of graph rewriting appear to be entirely new concepts, and yield powerful new approaches for both theory and applications. The focus of this talk will be the interplay between mathematical structure and some of these new approaches. The work presented is joint work with V. Danos and I. Garnier (LFCS/ENS Paris) and (in an earlier phase) T. Heindel (University of Copenhagen). [slides] [video]
  • 14:40: Mark Lawson (Heriot-Watt University): Inverse semigroups and étale groupoids show abstract
    I shall describe the adjunction between the category of inverse semigroups and that of étale groupoids and how this leads to a non-commutative version of Stone duality. [slides] [video]
  • 15:20: Tea
  • 15:40: Bob Atkey (University of Strathclyde): From parametricity to conservation laws, via Noether's theorem
    Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy is by Noether's theorem a consequence of a system's invariance under time-shifting.

    I will show a way to link Reynolds' relational parametricity with Noether's theorem. I'll discuss an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. I'll show, by constructing a relationally parametric model, that relational parametricity is enough to satisfy the hypotheses of Noether's theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system. [slides] [video]
  • 16:20: Christian Saemann (Heriot-Watt University): Categorical description of gauge theory
    I will describe a very general approach to higher gauge theory and higher gauged sigma models that allows for arbitrary higher groupoids as spacetimes, target spaces and higher gauge groups. Various applications to physics and in particularly string theory will be pointed out. At the end, I will list some of the important open problems in this context. [slides] [video]
  • 17:00: Gwendolyn Barnes (Heriot-Watt University): A category theoretic framework for noncommutative and nonassociative geometry
    Observations from flux compactifications of closed string theory suggest that a theory of gravity at quantum scales may be not only noncommutative but also nonassociative. Having an abstract understanding of geometry is one approach to help us to describe a noncommutative and nonassociative theory of gravity. In work together with Alexander Schenkel and Richard J. Szabo we have appealed to the tools of category theory to better understand the mathematical structures underlying noncommutative and nonassociative deformations of spacetime geometry. [slides] [video]
  • 17:40: Pub

Registration is free, but for catering purposes please email the local organiser Chris Heunen as soon as possible if you plan to attend.

You might also be interested in two events earlier in the week: WadlerFest 2016 on Monday and Tuesday, and LFCS30 on Tuesday and Wednesday.

Sponsored by