Categorical programming

分类规划

• 批准号: RGPIN-2014-04222
• 负责人: Cockett, Robin
• 金额: $ 1.89万
• 依托单位: University of Calgary
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=647872
• 关键词: Categorical; programming

My group at the University of Calgary explores programming paradigms and their formalisms. We are currently exploring formalisms for Quantum programming, Concurrent programming, and Low Complexity programming. In each area the aim is not only to provide a programming language or an account of computation but also a complete categorical semantics with its attendant proof theory and morphology. This entails contributions ranging from theoretical foundations through to programming language design and implementation.**Languages which implement formal settings such as these deliver, for their programs, guarantees of desirable properties (e.g. termination, feasibility, deadlock freedom etc.). However, these properties come at a cost: the languages enforce powerful yet uniform disciplines for thinking about programs which are often quite novel and far from current programming practice. Thus, the ability to express even common computational problems efficiently in these settings - their expressivity - is not immediately clear. My group uses prototype implementations to experiment with the programming languages for these settings, in order to understand the programming disciplines they enforce, and to explore their expressivity. **As one aspect of our work, in the next granting period, we propose to investigate the utility of differentials both in semantics and in programming languages themselves. Differentials appear both at a "macroscopic" level, as the differential of datatypes, and in a less well-understood way at a "microscopic" level, through the ability to differentiate programs themselves. The differential of a program gives important information about how it uses its resources. To date this ability has found utility mainly in semantic arguments about programs. We would like not only to further understand the semantic implications, but also to understand whether this ability to differentiate programs might not also have utility at the level of programming itself.

我在卡尔加里大学的小组探索编程范式及其形式。我们目前正在探索量子编程、并发编程和低复杂度编程的形式化。在每个领域的目标不仅是提供一种编程语言或计算的说明，而且还提供一个完整的范畴语义及其相应的证明理论和形态学。这需要从理论基础到编程语言设计和实现的贡献。**实现这些正式设置的语言为它们的程序提供了理想属性的保证（例如终止、可行性、无死锁等）。然而，这些特性是有代价的：这些语言强制执行强大而统一的规则来思考程序，这些程序通常非常新颖，与当前的编程实践相去甚远。因此，在这些设置中有效表达甚至常见计算问题的能力——它们的表达能力——并不是很清楚。我的团队使用原型实现对这些设置的编程语言进行实验，以便理解它们所执行的编程规则，并探索它们的表达能力。**作为我们工作的一个方面，在下一个授权期内，我们建议研究语义和编程语言本身的差异的效用。差异既表现在“宏观”层面，如数据类型的差异，也表现在“微观”层面，通过区分程序本身的能力，以一种不太容易理解的方式出现。程序的差异提供了关于程序如何使用其资源的重要信息。迄今为止，这种能力主要在关于程序的语义争论中发挥作用。我们不仅想进一步了解语义含义，而且想了解这种区分程序的能力是否在编程本身的层面上也没有效用。