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.
Rewriting modulo traced comonoid structure
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.
A compositional theory of digital circuits
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.
Rewriting Graphically With Symmetric Traced Monoidal Categories
Arxiv preprint
We examine a variant of hypergraphs with the aim of creating a sound
and complete graphical language for symmetric traced monoidal
categories.
A visualiser for linear lambda-terms as rooted 3-valent maps
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.
Talks
A Fully Compositional Theory of Sequential Digital Circuits
A Fully Compositional Theory of Sequential Digital Circuits
A Fully Compositional Theory of Sequential Digital Circuits
A Fully Compositional Theory of Digital Circuits
Rewriting modulo traced comonoid structure
A compositional theory of digital circuits
A compositional theory for digital circuits
Fully abstract categorical semantics for digital circuits
Normalisation by evaluation for digital circuits
Rewriting graphically with Cartesian traced categories
Diagrammatic semantics with symmetric traced monoidal categories
Diagrammatic semantics for digital circuits
A visualiser for linear lambda-terms as rooted 3-valent maps
Visits
Birmingham,
15-16 April 2024
Birmingham,
14 December 2023
Birmingham,
13 December 2023
Kiel,
November 27-December 01, 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
Tallinn,
March 30-31, 2020
Sheffield,
December 18, 2019
Leicester,
December 16-17, 2019
Versailles,
July 1-2, 2019
Teaching