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.