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.
Contact me
- g.j.kaye at cs.bham.ac.uk
- Office 244 (Desk J), School of Computer Science, University of Birmingham
Contributing
If you find a mistake, 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 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.
You might want to read mv CV.
News
Papers
Rewriting Graphically With Symmetric Traced Monoidal Categories
[
pdf]
[
arxiv]
[
bibtex]
[
abstract]
Arxiv preprint
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
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.
Talks
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
SYCO 8
Tallinn
December 13-14, 2021
SYCO 7
Tallinn
March 30-31, 2020
SYCO 6
Leicester
December 16-17, 2019
Teaching
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
Misc
Pictures
Pictures of me
Adventures in Academia
A series of entertaining escapades
Railway stations
I take pictures of station signs
Train simulator scenarios