Professor

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

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.