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.