Categorical programming

分类规划

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

我在卡尔加里大学的团队探索了编程范例及其形式主义。我们目前正在探索量子编程、并发编程和低复杂性编程的形式化。在每个领域中，其目标不仅是提供一种编程语言或计算的帐户，而且还提供一个完整的范畴语义及其伴随的证明理论和形态学。这需要做出从理论基础到编程语言设计和实施的各种贡献。 实现诸如这些形式设置的语言为其程序提供所需属性(例如，终止性、可行性、死锁自由等)的保证。然而，这些特性是有代价的：语言强制实施强大而统一的规则来思考程序，而这些程序通常是相当新颖的，与当前的编程实践相去甚远。因此，在这些环境中高效地表达常见计算问题的能力--它们的表现力--还不是很清楚。我的团队使用原型实现来试验针对这些环境的编程语言，以便了解它们所执行的编程规程，并探索它们的表现力。 作为我们工作的一个方面，在下一个授权期，我们建议调查差异在语义和编程语言本身中的效用。差异既出现在“宏观”级别，作为数据类型的差异，也出现在“微观”级别，通过区分程序本身的能力，以一种较少被理解的方式出现。程序的差异提供了有关如何使用其资源的重要信息。到目前为止，这种能力主要在关于程序的语义争论中找到了用处。我们不仅想进一步了解其中的语义含义，还想了解这种区分程序的能力是否也可能在编程本身的级别上具有实用价值。