Professor

教授

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

With the increased reliance of society on computer systems there is a commensurate fundamental requirement for formal programming systems which guarantee basic desirable properties through their type discipline. The foundations of these systems often devolves onto their categorical semantics. In this manner, category theory has become the primary mathematical tool for studying the structure and semantics of sequential, concurrent, probabilistic, quantum, and other computational systems. My group at Calgary has, for the past two decades, been studying the categorical semantics of a variety of systems with the aim of understanding how to deliver, through type systems and programming syntax, guarantees of desirable properties (such as termination, feasibility, deadlock/livelock freedom, etc.). This has entailed contributions ranging from the theoretical foundations through to programming language design and (prototype) implementation. ******This proposal focuses on three (related) aspects of this work -- categorical quantum mechanics, message passing concurrency, and differential programming. I intend to leverage advances in these and related areas opportunistically. The last period saw significant advances by my group in both categorical quantum mechanics and the semantics of differentiation: I use these as my starting point for this proposal. However, there has also been continued work on reversible computing and the foundations of computability some of which will reach fruition in the next grant period.**

随着社会对计算机系统的日益依赖，对形式化编程系统提出了相应的基本要求，这些系统通过其类型规则来保证基本的理想属性。 这些系统的基础往往是它们的范畴语义。 以这种方式，范畴论已经成为研究顺序、并发、概率、量子和其他计算系统的结构和语义的主要数学工具。 在过去的二十年里，我在卡尔加里的团队一直在研究各种系统的分类语义，目的是了解如何通过类型系统和编程语法来提供所需属性的保证（例如终止，可行性，死锁/活锁自由等）。 这需要从理论基础到编程语言设计和（原型）实现的贡献。** 本提案侧重于这项工作的三个（相关）方面-分类量子力学，消息传递并发性和差分编程。 我打算抓住机会利用这些领域和相关领域的进展。 在最后一个时期，我们小组在范畴量子力学和微分语义学方面都取得了重大进展：我将这些作为我提出这个建议的出发点。 然而，在可逆计算和可计算性基础方面也在继续开展工作，其中一些工作将在下一个赠款期取得成果。