Categorical programming

分类规划

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

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