Categorical Combinatorics for Proof Theory and Programming Languages.

一个长期存在的问题是理解计算机程序和数学证明的语义模型。这是一个理论问题，跨越了计算、终止程序和收敛的性质，但它有应用，因为它提出了使用编程语言的新方法，优化程序的新方法（用语义相同但更快的版本替换程序），以及验证程序正确性的新方法。该研究将在竞争性会议和期刊上发表。其主要目的是发展一种理论的作用，多范畴和丰富的范畴可以发挥广义版本的线性逻辑。线性在编程语言中至关重要，因为它限制了资源的使用方式。资源可能是传统编程中的内存指针，或量子计算中的量子位。范畴是一种给出一个组合的平等理论的方法。平等理论具有重要的理论意义。但它们在实践中也很重要，例如，它们形成了优化编译器转换的基础，例如类型定向部分求值，这使得程序运行得更快。组合性很重要，因为它意味着我们可以根据程序的各个部分来理解整个程序;同样，这在理论上很重要，但在实践中也很重要，因为它允许编译器优化程序的各个部分。第二个目的是探索这些语义结构的具体和计算形式化，在Agda类型系统的精神，和正在进行的“立方体”扩展Agda，Prover 9方程逻辑证明，和Globular图形证明助手。该方法是新颖的，因为它建立在S Staton及其合作者最近的发展基础上，这些发展是关于量子编程语言的分类模型，使用丰富的类别和组合物种的丰富（发表于MFPS 2017，POPL 2015）;关于前多类别和效应（POPL 2013）;以及可能是量子逻辑中的效应代数及其与预层范畴的关系（ICALP 2015）。研究员达里奥·斯泰因（Dario Stein）是做这项工作的理想人选，因为他已经修过范畴论、量子计算、组合学、代数几何、集合论、逻辑和群的可判定性等课程，并在剑桥攻读数学硕士学位时，写过一篇关于局部可呈现和可访问范畴的论文。他还熟悉该项目的更多实践方面，包括函数式语言（F#和Haskell）和工具（Prover 9）。

A long standing problem is to understand semantic models for computer programs, and for mathematical proofs. This is a theoretical problem, spanning the nature of computation, of terminating programs, and convergence, but it has applications as it suggests new ways of using programming languages, new ways of optimizing programs (replacing a program with a semantically identical but faster version), and new ways of verifying program correctness. The research will be published in competitive conferences and journals. The main aim is to develop a theory of the role that multicategories and enriched categories can play in generalized versions of linear logic. Linearity is crucial in programming languages because it constrains how resources are used. Resources might be memory pointers in conventional programming, or qubits in quantum computing. Categories are a way of giving a theory of equality that is compositional. Theories of equality are important philosophically. But they are also important in practice, for example, they form the basis of optimizing compiler transformations, such as type-directed-partial-evaluation, which make programs run faster. Compositionality is important because it means we can understand a whole program in terms of its parts; again, this is important philosophically, but also in practice, as it allows a compiler to optimize parts of the program. A secondary aim is to explore concrete and computational formalizations of these semantic structures, in the spirit of the Agda type system, and ongoing 'cubical' extensions of Agda, the Prover9 equational logic prover, and the Globular graphical proof assistant. The methodology is novel because it builds on recent developments by S Staton and collaborators on categorical models of quantum programming languages using enriched categories and enrichment in combinatorial species (published in MFPS 2017, POPL 2015); on premulticategories and effects (POPL 2013); and possibly on recent work on effect algebras in quantum logic and their relation to presheaf categories (ICALP 2015). The researcher, Dario Stein, is ideally placed to do this work, because he has taken courses on category theory, quantum computation, combinatorics, algebraic geometry, set theory, logic and decidability in groups, and written a dissertation on locally presentable and accessible categories, as part of his Masters in Mathematics at Cambridge. He is also familiar with more practical aspects of the project, including functional languages (F# and Haskell) and tools (Prover9).