权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Categorical Combinatorics for Proof Theory and Programming Languages.

证明理论和编程语言的分类组合。

基本信息

批准号：
1894512
负责人：
金额：
--
依托单位：
University of Oxford
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2017
资助国家：
英国
起止时间：
2017 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-1894512
关键词：
Categorical Combinatorics Proof Theory Programming

项目摘要

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

一个长期存在的问题是理解计算机程序和数学证明的语义模型。这是一个理论问题，跨越了计算、终止程序和收敛的本质，但它也有应用，因为它提出了使用编程语言的新方法、优化程序的新方法(用语义相同但更快的版本替换程序)和验证程序正确性的新方法。这项研究将在竞争性会议和期刊上发表。主要目的是发展一种理论，说明多范畴和丰富范畴在线性逻辑的广义版本中可以发挥的作用。线性在编程语言中至关重要，因为它限制了资源的使用方式。资源可能是传统编程中的内存指针，也可能是量子计算中的量子比特。范畴是一种给予平等理论的方式，这种理论是构成的。平等论在哲学上很重要。但它们在实践中也很重要，例如，它们构成了优化编译器转换的基础，例如类型定向部分求值，这些转换使程序运行得更快。组合性很重要，因为它意味着我们可以理解整个程序的各个部分；同样，这在哲学上很重要，但在实践中也很重要，因为它允许编译器优化程序的各个部分。第二个目标是在AGDA类型系统的精神下，探索这些语义结构的具体和计算形式化，以及正在进行的AGDA、Prover9等式逻辑证明器和球状图形证明助手的立方扩展。这种方法是新颖的，因为它建立在S·斯塔顿和他的合作者最近的发展基础上，即使用丰富的范畴和组合物种的丰富的量子编程语言的范畴模型(发表在MFPS 2017上，POPL2015)；关于前多范畴和效应(POPL2013)；以及可能建立在量子逻辑中的效应代数及其与前堆范畴的关系(ICALP 2015)的最新工作的基础上。这位名叫达里奥·斯坦(Dario Stein)的研究人员非常适合做这项工作，因为他在剑桥大学的数学硕士学位课程中，曾选修过范畴理论、量子计算、组合学、代数几何、集合论、逻辑和群组可判断性等课程，并撰写了一篇关于局部可表示和可达范畴的论文。他还熟悉该项目的更多实用方面，包括函数式语言(F#和Haskell)和工具(Prover9)。