Type systems for the Spartan Calculus

The aim of this project is to develop a sound and complete diagrammatic semantics for digital circuits, continuing on from the work by Ghica, Jung and Lopez. This will involve defining a graphical language (using 'hypergraphs'), then defining several operations on it (e.g. equivalence of graphs, how to composing graphs together). Once this language is formalised, a way of representing the equational representation of circuits developed in Ghica and Jung's 'Categorical semantics for digital circuits' in the graphical language must be developed. It must then be shown that every circuit can be represented as a well-formed diagram (soundness), and that every diagram represents a well-formed circuit (completeness).