Research

I used to do research before I went off to do software development instead. On this page you can find everything I did during that time; if you have any questions, please don't hesitate to reach out!

Research interests

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.

My PhD thesis detailed a fully compositional theory of sequential digital circuits with delay and feedback. This project was based on work by Ghica and Jung who modelled digital circuits as morphisms in a symmetric traced monoidal category. My job was to tidy this all up and make it formal, leading to three sound and complete semantics for sequential circuits: a denotational semantics of monotone stream functions, a reductions-based operational semantics, and an algebraic semantics. Using recent work on string diagram graph rewriting, this gives us a framework suitable for performing graph rewriting on digital circuits.

Papers

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
George Kaye
PhD thesis, University of Birmingham
This thesis details the culmination of a project to define a fully compositional theory of synchronous sequential circuits built from primitive components, motivated by applying techniques successfully used in programming languages to hardware. The first part of the thesis defines the syntactic foundations required to create sequential circuit morphisms, and then builds three different semantic theories on top of this: denotational, operational and algebraic. We characterise the denotational semantics of sequential circuits as certain causal stream functions, as well as providing a link to existing circuit methodologies by mapping between circuit morphisms, stream functions and Mealy machines. The operational semantics is defined as a strategy for applying some global transformations followed by local reductions in order to demonstrate how a circuit processes a value, leading to a notion of observational equivalence. The algebraic semantics consists of equations for bringing circuits into a pseudo-normal form, and then encoding between different state sets. This part of the thesis concludes with a discussion of some novel applications, such as those for using partial evaluation for digital circuits. While mathematically rigorous, the categorical string diagram formalism is not suited for reasoning computationally. The second part of this thesis details an extension of existing work on string diagram rewriting with hypergraphs so that it is compatible with the traced comonoid structure present in the category of digital circuits. We identify the properties that characterise cospans of hypergraphs corresponding to traced comonoid terms, and demonstrate how to identify rewriting contexts valid for rewriting modulo traced comonoid structure. We apply the graph rewriting framework to fixed point operators as well as the operational semantics from the first part, and present a new hardware description language based on these theoretical developments.
pdfbibtex
Rewriting modulo traced comonoid structure
Dan Ghica, George Kaye
FSCD 2023
We adapt the existing work on rewriting string diagrams using hypergraphs in order to apply it to settings with a traced comonoid structure, which happens to be where we model digital circuits.
paper(pdf)arxiv(pdf)bibtex
A compositional theory of digital circuits
Dan Ghica, George Kaye, David Sprunger
Arxiv preprint
We model digital circuits with delay and feedback as morphisms in a symmetric traced monoidal category, formalise their semantics as stream functions with certain properties, and present equational theory for reasoning with them.
arxiv(pdf)bibtex
Rewriting Graphically With Symmetric Traced Monoidal Categories
George Kaye, with Dan Ghica
Arxiv preprint
We examine a variant of hypergraphs with the aim of creating a sound and complete graphical language for symmetric traced monoidal categories.
arxiv(pdf)bibtex
A visualiser for linear lambda-terms as rooted 3-valent maps
George Kaye, supervised by Noam Zeilberger
Masters dissertation (2019), University of Birmingham
We detail the development of a set of tools to aid in the research of the topological properties of linear λ-terms when they are represented as 3-valent rooted maps.
pagepdfbibtex

Talks

A Fully Compositional Theory of Sequential Digital Circuits
7th International Conference on Applied Category Theory (ACT 2024), June 21, 2024
A Fully Compositional Theory of Sequential Digital Circuits
5th Meeting of the Southern and Midlands Logic Seminar, April 05, 2024
A Fully Compositional Theory of Sequential Digital Circuits
UCL PPLV seminar, February 15, 2024
A Fully Compositional Theory of Digital Circuits
SYNCHRON 2023, Kiel, November 27, 2023
Rewriting modulo traced comonoid structure
FSCD 2023, Rome, July 04, 2023
A compositional theory of digital circuits
Midlands Graduate School 2023, April 05, 2023
A compositional theory for digital circuits
LFCS seminar, Edinburgh, February 07, 2023
Fully abstract categorical semantics for digital circuits
ACT 2022, July 20, 2022
Normalisation by evaluation for digital circuits
SYCO 8, December 13, 2021
Rewriting graphically with Cartesian traced categories
ACT 2021, July 12, 2021
Diagrammatic semantics with symmetric traced monoidal categories
Huawei Edinburgh PL Group Tech Talk, March 04, 2021
Diagrammatic semantics for digital circuits
SYNCHRON 2020, November 27, 2020
A visualiser for linear lambda-terms as rooted 3-valent maps
CLA 2019, July 01, 2019

Visits

Oxford, 17-21 June 2024
Birmingham, 15-16 April 2024
Bath, 05 April 2024
Birmingham, 14 December 2023
Birmingham, 13 December 2023
Kiel, November 27-December 01, 2023
Rome, July 03-06, 2023
London, May 16, 2023
Paris, April 20-21, 2023
Bath, February 23, 2023
Edinburgh, January 24, 2023
Edinburgh, December 19-20, 2022
Glasgow, July 18-22, 2022
Nottingham, April 10-14, 2022
Tallinn, December 13-14, 2021
Cambridge, July 12-16, 2021
online, November 26-27, 2021
online, July 6-10, 2020
Tallinn, March 30-31, 2020
Sheffield, December 18, 2019
Leicester, December 16-17, 2019
Versailles, July 1-2, 2019

Teaching

Spring 2024
Spring 2022
Autumn 2021
Autumn 2020
Spring 2020 ocaml tutorial
Autumn 2019