Type systems for the Spartan Calculus

这个项目的目标是在Ghica，Jung和Lopez工作的基础上，为数字电路开发一个健全和完整的图形化语义。这将涉及定义一种图形语言(使用“超图”)，然后定义对其的几个操作(例如，图的等价性，如何将图组合在一起)。一旦这种语言被形式化，就必须开发一种用图形语言来表示在Ghica和Jung的《数字电路的范畴语义》中发展的电路的等式表示的方法。然后必须证明，每个电路可以表示为结构良好的图(完备性)，并且每个图表示结构良好的电路(完备性)。

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).