I am a member of the University of Birmingham Theory Group.
University: g.j.kaye at cs.bham.ac.uk
Where to find me: Office 244 (Desk J), School of Computer Science, University of Birmingham
My primary research interests are in graphical calculi for compositional systems and the lambda calculus using monoidal categories, and reasoning about these structures diagrammatically and by using graph rewriting techniques. I am also interested in general programming languages and compilers. On a more practical side, I enjoy making and experimenting with visualisers for various theoretical concepts.
Currently I am working on a diagrammatic semantics for digital circuits, motivated by the work of Ghica and Jung  . I am using a variant of hypergraphs that are a sound and complete calculus for symmetric traced monoidal categories. The ultimate aim of this project is to define an automatic rewriting system for these hypergraphs that we can use as an effective and efficient operational semantics for digital circuits.
When I’m not researching, I play the piano and go on adventures usually involving trains, canals or both. I occasionally take photos of pretty things and put them on Instagram. If you want something less pretty, here are some pictures of me! I also (very rarely) use Twitter.
I’m currently School of Computer Science Cookie Break admin! The Cookie Break is the School’s longest running social event and it’s an honour to be in charge of such an esteemed tradition.
You might want to read my CV.
Click a publication to read the abstract.
We examine a variant of hypergraphs that we call interfaced linear hypergraphs, with the aim of creating a sound and complete graphical language for symmetric traced monoidal categories (STMCs) suitable for graph rewriting. In particular, we are interested in rewriting for categorical settings with a Cartesian structure, such as digital circuits. These are incompatible with previous languages where the trace is constructed using a compact closed or Frobenius structure, as combining these with Cartesian product can lead to degenerate diagrams. Instead we must consider an approach where the trace is constructed as an atomic operation. Interfaced linear hypergraphs are defined as regular hypergraphs in which each vertex is the source and target of exactly one edge each, equipped with an additional interface edge. The morphisms of a freely generated STMC are interpreted as interfaced linear hypergraphs, up to isomorphism (soundness). Moreover, any linear hypergraph is the representation of a unique STMC morphism, up to the equational theory of the category (completeness). This establishes interfaced linear hypergraphs as a suitable combinatorial language for STMCs. We then show how we can apply the theory of adhesive categories to our graphical language, meaning that a broad range of equational properties of STMCs can be specified as a graph rewriting system. The graphical language of digital circuits is presented as a case study.
ACT 2021, Cambridge July 12-16, 2021
SYNCHRON 2020, online November 26-27, 2020
ACT 2020, online July 6-10, 2020
SYCO 7, Estonia March 30-31, 2020
MGS Christmas Seminar December 18, 2019
SYCO 6, Leicester December 16-17, 2019
CLA 2019, Versailles July 1-2, 2019
Mathematical and Logical Foundations of Computer Science University of Birmingham, teaching assistant
Mathematical Foundations of Computer Science University of Birmingham, teaching assistant
Pictures Pictures of me
Projects Some things I’ve done
Railway stations Photographing all the stations in Great Britain