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.**