$\newcommand{\nat}{\mathbb{N}}$ $\newcommand{\nat}{\mathbb{N}}$ $\newcommand{\mca}{\mathcal{A}}$ $\newcommand{\powerset}{\mathcal{P}}$ $\newcommand{\djf}{\oplus}$ $\newcommand{\ndjf}{\oslash}$ $\newcommand{\set}[1]{\underline{#1}}$ $\newcommand{\proj}[1]{\pi_#1}$ $\newcommand{\mf}[1]{\mathsf{#1}}$ $\newcommand{\torder}[1]{{{#1}_\leq}}$ $\newcommand{\comborder}{⧀}$ $\newcommand{\fall}[3]{\forall #1 \in #2 . \, #3}$ $\newcommand{\nor}{{\downarrow}}$ $\newcommand{\xor}{\oplus}$ $\newcommand{\pair}[2]{\langle #1,#2 \rangle}$ $\newcommand{\sig}{\Sigma_{\textbf{Circ}}}$ $\newcommand{\morph}[3]{#1 : #2 \to #3}$ $\newcommand{\lub}{\sqcup}$ $\newcommand{\latleq}{\sqsubseteq}$ $\newcommand{\latgeq}{\sqsupseteq}$ $\newcommand{\overbar}{\overline}$ $\newcommand{\args}[1]{\overbar{v_#1}}$ $\newcommand{\vals}{\overbar{v}}$ $\newcommand{\ubar}[1]{\underaccent{\bar}{#1}}$ $\newcommand{\seq}{\cdot}$ $\newcommand{\tensor}{\otimes}$ $\newcommand{\bigtensor}{\bigotimes}$ $\newcommand{\fork}{\curlywedge}$ $\newcommand{\join}{\curlyvee}$ $\newcommand{\stub}{{\sim}}$ $\newcommand{\swap}[2]{\times_{#1,#2}}$ $\newcommand{\dfork}[1]{\Delta_{#1}}$ $\newcommand{\djoin}[1]{\nabla_{#1}}$ $\newcommand{\delay}{\delta}$ $\newcommand{\trace}[2]{\text{Tr}^{#1}(#2)}$ $\newcommand{\iter}[2]{\text{iter}^{#1}(#2)}$ $\newcommand{\bb}[1]{\llb #1 \rrb}$ $\newcommand{\fix}[1]{\text{fix}(#1)}$ $\newcommand{\llb}{\llbracket}$ $\newcommand{\rrb}{\rrbracket}$ $\newcommand{\mcs}{\mathcal{S}}$ $\newcommand{\mcv}{\mathcal{V}}$ $\newcommand{\ecal}{\mathcal{E}}$ $\newcommand{\vcal}{\mathcal{V}}$ $\newcommand{\edges}{E}$ $\newcommand{\vt}{V^{\mathcal{T}}}$ $\newcommand{\vs}{V^{\mathcal{S}}}$ $\newcommand{\vleft}{\lambda}$ $\newcommand{\vright}{\rho}$ $\newcommand{\vtorder}{{\leq^{\mathcal{T}}}}$ $\newcommand{\vsorder}{{\leq^{\mathcal{S}}}}$ $\newcommand{\vtordern}[1]{{\leq^{\mathcal{T}}_#1}}$ $\newcommand{\vsordern}[1]{{\leq^{\mathcal{S}}_#1}}$ $\newcommand{\einput}{\alpha}$ $\newcommand{\eoutput}{\omega}$ $\newcommand{\vconnsr}{\kappa}$ $\newcommand{\vconnsl}{\kappa^{-1}}$ $\newcommand{\lcal}{\mathcal{L}}$ $\newcommand{\labels}{\Lambda}$ $\newcommand{\hyper}{((\vt, \vtorder), (\vs, \vsorder), E, \einput, \eoutput, vleft, \vright, \vconnsr, L, \labels)}$ $\newcommand{\hypern}[1]{((\vt_#1, \vtordern{#1}), (\vs_#1, \vsordern{#1}), E_#1, \einput_#1, \eoutput_#1, \vleft_#1, \vright_#1, \vconnsr_#1, L_#1, \labels_#1)}$ $\newcommand{\esources}{\mathsf{s}}$ $\newcommand{\etargets}{\mathsf{t}}$ $\newcommand{\rename}{\pi}$ $\newcommand{\renameinv}{\rename^{-1}}$ $\newcommand{\connsr}{f_{\rightarrow}}$ $\newcommand{\connsl}{f_{\leftarrow}}$ $\newcommand{\whomo}[2]{\leadsto^{#1}_{#2}}$ $\newcommand{\hwhomo}{\approx_h}$ $\newcommand{\hequiv}{\equiv_\mathsf{h}}$ $\newcommand{\hhomo}[2]{h_{#1\to#2}}$ $\newcommand{\circtochyp}{\varphi}$ $\newcommand{\chyptocirc}{\psi}$ $\newcommand{\inport}[2]{(#1,#2)^S}$ $\newcommand{\outport}[2]{(#1,#2)^T}$ $\newcommand{\vmaps}{\mathsf{vmap}^{\mathcal{S}}}$ $\newcommand{\vmapss}{\mathsf{vmap}^{\mathcal{S*}}}$ $\newcommand{\vmapt}{\mathsf{vmap}^{\mathcal{T}}}$ $\newcommand{\vmapts}{\mathsf{vmap}^{\mathcal{T*}}}$ $\newcommand{\emap}{\mathsf{emap}}$ $\newcommand{\id}{\mathsf{id}}$ $\newcommand{\agda}[2]{\texttt{[}#1\texttt{.#2.agda]}}$ $\newcommand{\uinfix}[1]{\texttt{\_}#1\texttt{\_}}$
Welcome to my website!

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 Theory Group.

Contact me

University: g.j.kaye at cs.bham.ac.uk

Where to find me: Office 244 (Desk J), School of Computer Science, University of Birmingham

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 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 [1] [2]. 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.

The Graphical Language of Symmetric Traced Monoidal Categories [pdf] [arxiv] [bibtex]
Arxiv preprint with Dan Ghica

We examine a variant of hypergraphs that we call linear hypergraphs, with the aim of creating a sound and complete graphical language for symmetric traced monoidal categories (STMCs). We first define the category of linear hypergraphs as a full subcategory of conventional (simple) hypergraphs, in which each vertex is either the source or the target of exactly one edge. The morphisms of a freely generated STMC can be then interpreted as 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 linear hypergraphs as the graphical language of STMCs. Linear hypergraphs are then shown to form a partial adhesive category which means that a broad range of equational properties of some STMC can be specified as a graph rewriting system. The graphical language of digital circuits is presented as a case study.

Masters project

A visualiser for linear lambda-terms as rooted 3-valent maps [page] [pdf]
Masters dissertation 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.


Diagrammatic Semantics for Digital Circuits
SYNCHRON 2020 November 27, 2019 [slides]

The Graphical Language of Symmetric Traced Monoidal Categories
Birmingham Theory PhD Seminar November 23, 2019 [slides]

Diagrammatic Semantics for Digital Circuits (basic talk)
Research skills presentation January 27, 2020 [slides]

A visualiser for linear lambda-terms as rooted 3-valent maps
CLA 2019 July 1, 2019 [slides]


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


Compilers & Languages University of Birmingham, teaching assistant [ocaml tutorial]

Mathematical Foundations of Computer Science University of Birmingham, teaching assistant




Train simulator scenarios