$\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{\_}}$
 
Hello!
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.

fadd.svg

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.

Projects

Diagrammatic semantics for digital circuits [Visualiser] [Very basic talk]
Defining an operational semantics for digital circuits using hypergraphs.

A visualiser for linear lambda-terms as rooted 3-valent maps [Page]
A set of tools for the representation of lambda terms as their corresponding rooted maps. Developed for my MSci final year project under the supervision of Noam Zeilberger.

Other projects

Talks

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

Visits

ACT 2020, The internet 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

Teaching

2019-20

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

Mathematical Foundations of Computer Science University of Birmingham, teaching assistant

Misc

Pictures

Train simulator scenarios