Type systems for the Spartan Calculus

斯巴达微积分的类型系统

• 批准号: 2273985
• 金额: --
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2273985
• 关键词: Type; systems; 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).

该项目的目的是为数字电路开发一个健全和完整的图解语义，继续Ghica， Jung和Lopez的工作。这将涉及定义一种图形语言（使用“超图”），然后定义几种操作（例如图的等价，如何将图组合在一起）。一旦这种语言被形式化，就必须用图形语言来表示在Ghica和Jung的“数字电路的绝对语义”中发展出来的电路的等式表示。然后必须证明每个电路都可以表示为一个格式良好的图（健全性），并且每个图都表示一个格式良好的电路（完整性）。