Welcome to my website!

A picture of me, with the Forth Bridge in the background

A picture of me, with the Forth Bridge in the background

Hello! I’m George, a PhD student researcher at the University of Birmingham, under the supervision of Dan Ghica and Miriam Backens.

I am a member of the University of Birmingham Theory Group. Along with Tom de Jong, I organise the research group's weekly seminar and maintain its website.

Contact me


If you find a mistake, make an issue and I'll try to sort it out. Alternatively, you can fix it yourself with a pull request!

About me

My primary research interests are in graphical calculi for compositional systems and the lambda calculus using monoidal categories, and reasoning about these structures diagrammatically using string diagrams and graph rewriting. I am also interested in programming languages and compilers, as well as making and experimenting with visualisers for various theoretical concepts.

Currently I am working on developing the categorical semantics for digital circuits with delay and feedback first presented by Ghica and Jung using symmetric traced monoidal categories. This gives us a graphical calculas with which we can reason about circuits syntactically.

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 use Twitter.

You might want to read mv CV.


26 January 2022
Put a new preprint on the arxiv, 'Full abstraction for digital circuits'!
13 December 2021
Attended SYCO 8 in Tallinn and gave a talk on 'Normalisation by evaluation for digital circuits'.
10 December 2021
After many months of wrestling with Contensis, we finally managed to get the first batch of Birmingham computer science PhD students profiles on the university website! Thanks must also go to Tom de Jong who helped me proofread them all. You can see the list at https://www.birmingham.ac.uk/schools/computer-science/people/research-students.aspx.


Full abstraction for digital circuits [pdf] [arxiv] [bibtex] [abstract]
Arxiv preprint

Dan Ghica, George Kaye, David Sprunger

This paper refines the existing axiomatic semantics of digital circuits with delay and feedback, in which circuits are constructed as morphisms in a freely generated cartesian traced (dataflow) category. First, we give a cleaner presentation, making a clearer distinction between syntax and semantics, including a full formalisation of the semantics as stream functions. As part of this effort, we refocus the categorical framework through the lens of string diagrams, which not only makes reading equations more intuitive but removes bureaucracy such as associativity from proofs. We also extend the existing framework with a new axiom, inspired by the Kleene fixed-point theorem, which allows circuits with non-delay-guarded feedback, typically handled poorly by traditional methodologies, to be replaced with a series of finitely iterated circuits. This eliminates the possibility of infinitely unfolding a circuit; instead, one can always reduce a circuit to some (possibly undefined) value. To fully characterise the stream functions that correspond to digital circuits, we examine how the behaviour of the latter can be modelled using Mealy machines. By establishing that the translation between sequential circuits and Mealy machines preserves their behaviour, one can observe that circuits always implement monotone stream functions with finite stream derivatives.

Rewriting Graphically With Symmetric Traced Monoidal Categories [pdf] [arxiv] [bibtex] [abstract]
Arxiv preprint

George Kaye, with Dan Ghica

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.

A visualiser for linear lambda-terms as rooted 3-valent maps [page] [bibtex] [abstract]
Masters dissertation (2019), University of Birmingham

George Kaye, supervised by Noam Zeilberger

We detail the development of a set of tools in Javascript to aid in the research of the topological properties of linear λ-terms when they are represented as 3-valent rooted maps. A λ-term visualiser was developed to visualise a λ-term specified by the user as a rooted map on the screen. The visualiser also includes functionality related to normalisation of terms, such as the option to view a normalisation graph or reduce a term to its normal form. To complement this a λ-term gallery was created to generate λ-terms that satisfied criteria specified by the user, and display their corresponding maps. While the focus of the project was on linear λ-terms, these tools also work for all pure λ-terms. The tools can be used for a variety of different applications, such as examining the structure of different terms, disproving conjectures regarding various subsets of the λ-calculus, or investigating special normalisation properties held by different sets of λ-terms. We evaluate the tools’ success and acknowledge that while the tools suffer from performance issues when used for larger terms, they still fulfil many of the original aims of the project, and may still be very useful for systematic exploration of the λ-calculus in the future.


Fully abstract categorical semantics for digital circuits
ACT 2022 July 18, 2022 [extended abstract] [github]
Normalisation by Evaluation for Digital Circuits
SYCO 8 December 13, 2021 [slides] [extended abstract] [github]
Rewriting Graphically with Cartesian Traced Categories
ACT 2021 July 12, 2021 [slides] [extended abstract] [video]
Diagrammatic Semantics with Symmetric Traced Monoidal Categories
Huawei Edinburgh PL Group Tech Talk March 04, 2021 [slides] [video]
Diagrammatic Semantics for Digital Circuits
SYNCHRON 2020 November 27, 2020 [slides] [video]
A visualiser for linear lambda-terms as rooted 3-valent maps
CLA 2019 July 01, 2019 [slides]


MGS 2022 Nottingham April 10-14, 2022
SYCO 8 Tallinn December 13-14, 2021
ACT 2021 Cambridge July 12-16, 2021
SYNCHRON 2020 online November 26-27, 2021
ACT 2020 online July 6-10, 2020
SYCO 7 Tallinn March 30-31, 2020
MGS Christmas Seminar 2019 Sheffield December 18, 2019
SYCO 6 Leicester December 16-17, 2019
CLA 2019 Versailles July 1-2, 2019


Spring 2022 Teaching assistant University of Birmingham
Autumn 2021 Teaching assistant University of Birmingham
Autumn 2020 Teaching assistant University of Birmingham
Spring 2020 Teaching assistant University of Birmingham [ocaml tutorial]
Autumn 2019 Teaching assistant University of Birmingham


Pictures Pictures of me

Adventures in Academia A series of entertaining escapades

Railway stations I take pictures of station signs

Train simulator scenarios